diff --git a/test/test-sat3.js b/test/test-sat3.js new file mode 100644 index 0000000..f45c2b0 --- /dev/null +++ b/test/test-sat3.js @@ -0,0 +1,60 @@ +var L = sat.L + +var t1=time(),t2,t3 + +var m = sat.solver() + +var i,j,i2,j2,row +var locations=[] +for (i=0;i<9;i++) { + row=[] + for(j=0;j<9;j++) { + row.push(sat.L.variableBits([i,j], 4)); + } + locations.push(row) +} + + +var bits = [] +for(i=0;i<10;i++) bits[i]= L.constantBits(i); + + +for (i=0;i<9;i++) { + for (j=0;j<9;j++) { + sat.R(m,L.greaterThanOrEqual(locations[i][j], bits[1])) + sat.R(m,L.lessThanOrEqual(locations[i][j], bits[9])) + for(j2=0;j2<9;j2++) { + if (j !== j2) { + sat.F(m,L.equalBits(locations[i][j], locations[i][j2])) + } + } + } + for(i2=0;i2<9;i2++) { + for (j=0;j<9;j++) { + if (i !== i2) { + sat.F(m,L.equalBits(locations[i][j], locations[i2][j])) + } + } + } +} + +// Presets +sat.R(m,L.equalBits(locations[0][0],bits[2])) +sat.R(m,L.equalBits(locations[1][0],bits[3])) +sat.R(m,L.equalBits(locations[0][1],bits[3])) +sat.R(m,L.equalBits(locations[8][8],bits[3])) + +t2=time() +sat.solve(m) +t3=time() +for (i=0;i<9;i++) { + var row='' + for (j=0;j<9;j++) { + row = row + ' ' + sat.eval(m,locations[i][j]); + } + print(row) +} + +print() +print('Setup time: '+(t2-t1)+' ms') +print('Solver time: '+(t3-t2)+' ms')