z3：解决八皇后之谜答案

【问题标题】：z3: solve the Eight Queens puzzlez3：解决八皇后之谜
【发布时间】：2019-06-25 00:36:11
【问题描述】：

我正在使用 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"

它返回：

failed to solve

代码有什么问题？

谢谢！

【问题讨论】：

标签： python z3 smt z3py

【解决方案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 时才满足。在您对问题的表述中，只有当 i, j 对等于 k, h 时，X[i][j] == 1 和 X[k][h] == 1 永远不会出现这种情况，也就是说，如果X[i][j] = 1 永远不会出现这种情况对于任何i, j。但是后一条规则违反了 rows 和 columns 基数约束，这些约束要求每个 column/row 存在于以免一个单元格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 单元格。此外，由于索引空间的对称性，每个约束都会“完全相同”生成两次。但是，每个单元格与少于 2*n 的其他单元格发生冲突（一些与少于 n 的单元格发生冲突），因此引入这么多在搜索过程中没有提供任何有用贡献的子句看起来有点矫枉过正，除了放慢速度。也许一种更具可扩展性的方法是对 rows 和 columns 以及 diagonals 使用基数约束（即Sum）。

【讨论】：