4 ms·
I like your Prolog solution! I thought I'd take a crack at a Python SAT-solver solution, also done in less than 1 second. from z3 import * # we use '-1'
by ZephyrP 9y ago
I like your Prolog solution! I thought I'd take a crack at a Python SAT-solver solution, also done in less than 1 second.
from z3 import *
# we use '-1' for empty
instance = ((-1,-1,-1,-1,-1,1,-1,-1,-1,1),
(1,-1,-1,-1,-1,-1,-1,0,-1,-1),
(-1,-1,0,-1,-1,-1,-1,0,-1,-1),
(-1,0,0,-1,-1,-1,0,-1,-1,1),
(1,-1,-1,-1,-1,-1,-1,-1,-1,1),
(-1,-1,-1,0,-1,-1,1,-1,-1,-1),
(0,-1,-1,-1,-1,1,-1,-1,-1,-1),
(-1,-1,-1,-1,-1,-1,-1,0,-1,0),
(0,-1,-1,-1,-1,-1,-1,-1,-1,0),
(-1,0,-1,0,-1,1,-1,-1,-1,-1))
size = len(instance)
# we could use bitvecs here too
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(size) ]
for i in range(size) ]
# each cell is a 1 or a 0
cells_c = [ And(0 <= X[i][j], X[i][j] <= 1) for i in range(size) for j in range(size) ]
# each row contains as many 1s as 0s
rows_c = [ Sum(X[i]) == size / 2 for i in range(size) ]
# each column contains as many 1s as 0s
cols_c = [ (Sum([ X[i][j] for i in range(size) ]) == size / 2)
for j in range(size) ]
# each cell can only have 2 neighbors sharing it's number.
rows_not_alike = [ If(X[i][j] == X[i][j-1], X[i][j+1] != X[i][j-1], True) for i in range(size)
for j in range(size-1) ]
cols_not_alike = [ If(X[i][j] == X[i-1][j], X[i-1][j] != X[i+1][j], True) for i in range(size-1)
for j in range(size) ]
puzzle_c = cells_c + rows_c + cols_c + rows_not_alike + cols_not_alike
instance_c = [ If(instance[i][j] == -1, True, X[i][j] == instance[i][j]) for i in range(size) for j in range(size) ]
s = Solver()
s.add(puzzle_c + instance_c)
print s.to_smt2()
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(size) ] for i in range(size) ]
print_matrix(r)
else:
print "failed to solve"
Generates:
[[0, 1, 0, 1, 0, 1, 0, 1, 0, 1],
[1, 0, 1, 0, 1, 0, 1, 0, 1, 0],
[0, 1, 0, 1, 1, 0, 1, 0, 1, 0],
[1, 0, 0, 1, 0, 1, 0, 1, 0, 1],
[1, 0, 1, 0, 1, 0, 0, 1, 0, 1],
[0, 1, 1, 0, 1, 0, 1, 0, 1, 0],
[0, 1, 0, 1, 0, 1, 0, 1, 0, 1],
[1, 0, 1, 0, 0, 1, 1, 0, 1, 0],
[0, 1, 0, 1, 1, 0, 0, 1, 1, 0],
[1, 0, 1, 0, 0, 1, 1, 0, 0, 1]]
- KGIII 9y agoThis may be frowned upon, but the above post and the parent post are why I visit, even if I don't comment much.
- zmonx 9y agoVery nice! I see you are using a way to express the constrant "at most two cells of the same value in direct succession in each row and column " that is shorter than the formulation I have posted. I used a conjunction of two constraints, for each triple of cells A, B, C in direct succession: ( A #= B ) #==> ( C #\= B ), ( B #= C ) #==> ( B #\= A ) And you are using only one constraint: B #= A #==> C #\= A To the SAT purist, the question may now arise: Are these ways really equivalent, do they state the same constraint? One way to check it is to apply CLP(B): Constraint Logic Programming over Boolean variables, which ships for example in SICStus Prolog and is provided as library(clpb). Using this library, we can ask: ?- taut((((A =:= B) =< ( C =\= B))* ((B =:= C) =< ( B =\= A))) =:= ((B =:= A) =< ( C =\= A)), T). This asks whether it is a tautology (taut/2) that the two ways to express the constraint are equivalent. The system answers: T = 1, sat(A=:=A), sat(B=:=B), sat(C=:=C). So: Yes, the two ways are in fact equivalent, because this equivalence always holds. Yours being shorter, I would in fact prefer it and could also use it in the Prolog solution! Well done! One additional neat thing about the Prolog solution: Since no further solution is found on backtracking in this case, we have in fact also verified that the reported solution is indeed unique. I suppose this check could also be added to your solution somehow to make such observations possible? For example, suppose I modify the puzzle to read: puzzle([[_,_,_,_,_,_,_,_,_,1], [1,_,_,_,_,_,_,0,_,_], [_,_,0,_,_,_,_,0,_,_], [_,0,0,_,_,_,0,_,_,1], [1,_,_,_,_,_,_,_,_,1], [_,_,_,0,_,_,1,_,_,_], [0,_,_,_,_,1,_,_,_,_], [_,_,_,_,_,_,_,0,_,0], [0,_,_,_,_,_,_,_,_,0], [_,0,_,0,_,1,_,_,_,_]]). Then there are 144 solutions (I have removed the first "1" from the first row), which I can generate with the Prolog solution within a second.