From 53576589ce869d44f46ce1ee0eb185044230940b Mon Sep 17 00:00:00 2001
From: sbosse <sbosse@uni-bremen.de>
Date: Tue, 27 Aug 2024 00:14:57 +0200
Subject: [PATCH] Tue 27 Aug 00:14:56 CEST 2024

---
 test/test-sat2.js | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 test/test-sat2.js

diff --git a/test/test-sat2.js b/test/test-sat2.js
new file mode 100644
index 0000000..dd6563a
--- /dev/null
+++ b/test/test-sat2.js
@@ -0,0 +1,46 @@
+// 3x3 SQUARE Solver
+// sat { R: require rule, L: Logic, F: forbid rule } 
+var L = sat.L 
+
+var m = sat.solver()
+var A = sat.L.variableBits('A', 4);
+var B = sat.L.variableBits('B', 4);
+var C = sat.L.variableBits('C', 4);
+var D = sat.L.variableBits('D', 4);
+var E = sat.L.variableBits('E', 4);
+var F = sat.L.variableBits('F', 4);
+var G = sat.L.variableBits('G', 4);
+var H = sat.L.variableBits('H', 4);
+var I = sat.L.variableBits('I', 4);
+
+var locations = [A, B, C, D, E, F, G, H, I];
+
+var ONE  = L.constantBits(1);
+var NINE = L.constantBits(9);
+var FIFTEEN = L.constantBits(15);
+
+[[A,B,C], [D,E,F], [G,H,I], [A,D,G], [B,E,H], [C,F,I],
+ [A,E,I], [G,E,C]].forEach(
+       function (terms) {
+         sat.R(m,L.equalBits(L.sum(terms), FIFTEEN))
+       })
+
+locations.forEach(function (loc) {
+  sat.R(m,L.greaterThanOrEqual(loc, ONE))
+  sat.R(m,L.lessThanOrEqual(loc, NINE))
+})
+
+locations.forEach(function (loc1, i) {
+  locations.forEach(function (loc2, j) {
+    if (i !== j) {
+      sat.F(m,L.equalBits(loc1, loc2))
+    }
+  })
+})
+
+sat.solve(m)
+
+print([A,B,C].map(function (loc) { return sat.eval(m,loc)}).join(' '))
+print([D,E,F].map(function (loc) { return sat.eval(m,loc)}).join(' '))
+print([G,H,I].map(function (loc) { return sat.eval(m,loc)}).join(' '))
+