Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

z3: solve the Eight Queens puzzle

Tags:

python

z3

smt

z3py

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!

like image 281
Alfred Tan Avatar asked Dec 30 '17 06:12

Alfred Tan


1 Answers

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.

like image 159
Patrick Trentin Avatar answered Sep 26 '22 18:09

Patrick Trentin