diff --git a/test/test-sat4.js b/test/test-sat4.js new file mode 100644 index 0000000..d809c37 --- /dev/null +++ b/test/test-sat4.js @@ -0,0 +1,60 @@ +// 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); + +if (0) [[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(' ')); + +var m2 = JSON.parse(JSON.stringify(m)) +m2.id=null; + +[[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(m2,L.equalBits(L.sum(terms), FIFTEEN)) + }) + +sat.solve(m2) + +print([A,B,C].map(function (loc) { return sat.eval(m2,loc)}).join(' ')) +print([D,E,F].map(function (loc) { return sat.eval(m2,loc)}).join(' ')) +print([G,H,I].map(function (loc) { return sat.eval(m2,loc)}).join(' '))