Tue 27 Aug 00:14:56 CEST 2024

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')