I'm using Z3 to solve the Eight Queens puzzle. I know that each queen can be represented by a single integer in this problem. But, when I represent a queen by two integers as following:
from z3 import *
X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(8)] for i in range(8) ]
cells_c = [Or(X[i][j] == 0, X[i][j] == 1) for i in range(8) for j in range(8) ]
rows_c = [Sum(X[i]) == 1 for i in range(8)]
cols_c = [Sum([X[i][j] for i in range(8)]) == 1 for j in range(8) ]
diagonals_c = [Implies(And(X[i][j] == 1, X[k][h] == 1), abs(k - i) != abs(j - h))
for i in range(8) for j in range(8)
for k in range(8) for h in range(8)]
eight_queens_c = cells_c + rows_c + cols_c + diagonals_c
s = Solver()
s.add(eight_queens_c)
if s.check() == sat:
m = s.model()
r = [[m.evaluate(X[i][j]) for j in range(8)] for i in range(8)]
print_matrix(r)
else:
print "failed to solve"
it returns:
failed to solve
What's wrong with the code?
Thanks!
You problem is over-constrained due to the following piece of code:
diagonals_c = [Implies(And(X[i][j] == 1, X[k][h] == 1), abs(k - i) != abs(j - h))
for i in range(8) for j in range(8)
for k in range(8) for h in range(8)]
Whenever the pair i, j
is equal to k, h
then
abs(k - i) = 0 = abs(j - h)
and the implication conclusion is False
.
An implication with a False
conclusion is satisfied only when its premise is False
too. In your formulation of the problem, this is only possible if it is never the case that X[i][j] == 1
and X[k][h] == 1
whenever the pair i, j
is equal k, h
, that is, if it is never the case that X[i][j] = 1
for any i, j
. But the latter rule violates the rows and columns cardinality constraints which require that for each column/row there exists at lest one cell X_i_j
s.t. X_i_j = 1
. Thus, the formula is unsat
.
To solve this, a minimal fix is to simply exclude the case in which X[i][j]
and X[k][h]
refer to the same cell:
diagonals_c = [Implies(And(X[i][j] == 1, X[k][h] == 1,
i != k, j != h), abs(k - i) != abs(j - h))
for i in range(8) for j in range(8)
for k in range(8) for h in range(8)]
After this change, a solution is found.
e.g.
~$ python queens.py
[[0, 0, 0, 0, 1, 0, 0, 0],
[0, 0, 0, 0, 0, 0, 1, 0],
[0, 0, 0, 1, 0, 0, 0, 0],
[1, 0, 0, 0, 0, 0, 0, 0],
[0, 0, 1, 0, 0, 0, 0, 0],
[0, 0, 0, 0, 0, 0, 0, 1],
[0, 0, 0, 0, 0, 1, 0, 0],
[0, 1, 0, 0, 0, 0, 0, 0]]
NOTE: in your encoding of diagonals_c
, you introduce n*n
constraints for each cell, and there are n*n
cells in your problem. In addition, due to symmetries in the index space, each constraint is generated 'exactly the same' twice. However, each cell conflicts with fewer than 2*n
other cells (some conflict with fewer than n
), so it looks like a bit of an overkill to introduce so many clauses that don't provide any useful contribution along the search, except that of slowing it down. Perhaps a more scalable approach would be that of employing cardinality constraints (i.e. Sum
) not only for rows and columns but also for diagonals.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With