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, h然后

 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的i, j的情况。但是后一条规则违反了行和列的基数约束，这些约束要求对于每个列/行存在至少一个单元格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)]

在此更改后，找到解决方案。

EG

~$ 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），因此引入如此多的条款看起来有点过分，这些条款在搜索中没有提供任何有用的贡献，除了减慢它失败了。也许更可扩展的方法是采用基数约束（即Sum），不仅用于行和列，还用于对角线。