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"

它返回：

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, hthen

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

和蕴涵结论是False。

具有False结论的蕴涵只有在其前提False也成立时才得到满足。在您对问题的表述中，这只有在永远不会出现这种情况X[i][j] == 1并且X[k][h] == 1当这对i, j相等时才有可能k, h，也就是说，如果X[i][j] = 1对于 any从来都不是这种情况i, j。但后一条规则违反了行和列基数约束，该约束要求每一列/行至少存在一个单元格X_i_j st X_i_j = 1。因此，公式为unsat。

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

 abs(k - i) = 0 = abs(j - 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)]

注意：在您的 编码中diagonals_c，您n*n为每个单元格引入了约束，并且n*n您的问题中有单元格。此外，由于索引空间中的对称性，每个约束生成两次“完全相同”。但是，每个单元格与少于2*n其他单元格的冲突（有些与少于 冲突n），因此引入这么多在搜索过程中没有提供任何有用贡献的子句似乎有点矫枉过正，除了减慢搜索速度. 或许更可扩展的方法是使用基数约束（即Sum）不仅针对行和列而且针对对角线。