z3:解决八皇后难题 [英] z3: solve the Eight Queens puzzle

问题描述

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

I'm using Z3 to solve the Eight Queens puzzle. I know that each queen can be represented by a single integer in this problem. But, when I represent a queen by two integers as following:

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

代码有什么问题?

谢谢！

推荐答案

由于以下代码段，您的问题过度约束:

You problem is over-constrained due to the following piece of code:

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 时，则

Whenever the pair i, j is equal to k, h then

 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.但是后一条规则违反了 rows 和 columns 基数约束，这要求对于每个 column/row 存在于至少一个单元格 X_i_j stX_i_j = 1.因此，公式是unsat.

An implication with a False conclusion is satisfied only when its premise is False too. In your formulation of the problem, this is only possible if it is never the case that X[i][j] == 1 and X[k][h] == 1 whenever the pair i, j is equal k, h, that is, if it is never the case that X[i][j] = 1 for any i, j. But the latter rule violates the rows and columns cardinality constraints which require that for each column/row there exists at lest one cell X_i_j s.t. X_i_j = 1. Thus, the formula is unsat.

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

To solve this, a minimal fix is to simply exclude the case in which X[i][j] and X[k][h] refer to the same cell:

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

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

After this change, a solution is found.

例如

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

---

NOTE: in your encoding of diagonals_c, you introduce n*n constraints for each cell, and there are n*n cells in your problem. In addition, due to symmetries in the index space, each constraint is generated 'exactly the same' twice. However, each cell conflicts with fewer than 2*n other cells (some conflict with fewer than n), so it looks like a bit of an overkill to introduce so many clauses that don't provide any useful contribution along the search, except that of slowing it down. Perhaps a more scalable approach would be that of employing cardinality constraints (i.e. Sum) not only for rows and columns but also for diagonals.

这篇关于z3:解决八皇后难题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！