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

经过这次改动，找到了解决方案。

例如

~$ 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) .