z3: solve the Eight Queens puzzle

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!

Solution

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.