z3：解决八皇后难题

Question

我正在使用 Z3 解决八皇后难题。我知道在这个问题中每个皇后都可以用一个整数表示。但是，当我用以下两个整数表示女王时：

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"

它returns:

failed to solve

代码有什么问题？

谢谢！

Answer 1

由于以下代码，您的问题是过度约束：

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)]

只要 i, j 对等于 k, h 那么

 abs(k - i) = 0 = abs(j - h)

而蕴涵结论为False。

具有False结论的蕴涵只有在其前提也是False时才成立。在您对问题的表述中，这只有在 X[i][j] == 1 和 X[k][h] == 1 永远不会出现 i, j 对等于 k, h 的情况下才有可能，也就是说，如果它对于任何 i, j，从来没有 X[i][j] = 1 的情况。但是后一条规则违反了 rows 和 columns 基数约束，这些约束要求每个 column/行至少存在一个单元格X_i_j s.t。 X_i_j = 1。因此，公式为 unsat.

为了解决这个问题，一个最小的修复是简单地排除 X[i][j] 和 X[k][h] 指的是同一个单元格的情况：

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)]

这样修改后，找到解决办法了。

例如

~$ 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]]

注意： 在你对 diagonals_c 的编码中，你为每个单元格引入了 n*n 约束，并且你的代码中有 n*n 个单元格问题。此外，由于索引 space 中的对称性，每个约束生成 'exactly the same' 两次。但是，每个单元格与少于 2*n 个其他单元格发生冲突（有些冲突少于 n 个），因此引入这么多没有提供任何有用贡献的子句看起来有点矫枉过正沿着搜索，除了减慢速度。也许更具可扩展性的方法是不仅对行和列而且对对角线.

z3：解决八皇后难题

z3: solve the Eight Queens puzzle

python

smt

z3

z3py