Tue 27 Aug 00:14:56 CEST 2024
This commit is contained in:
parent
5a66abcb27
commit
194ba79223
60
test/test-sat4.js
Normal file
60
test/test-sat4.js
Normal file
|
@ -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(' '))
|
Loading…
Reference in New Issue
Block a user