61 lines
1.1 KiB
JavaScript
61 lines
1.1 KiB
JavaScript
|
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')
|