基于Z3的N皇后问题命题逻辑约束实现unsat问题排查

核心问题分析 #

你的代码返回unsat的原因集中在约束遗漏和循环逻辑错误两方面：

1. 遗漏对角线约束 #

最终组合约束时仅使用了Q1 + Q2 + Q3，完全漏掉了Q4、Q5对应的对角线约束。N皇后问题要求同一对角线上不能有两个皇后，这是必选约束，缺失后无法得到合法解。

2. Q5的约束构造错误 #

• Q5中直接将Z列表加入约束，而非将Z内的所有子约束用And连接后加入；
• k循环从0开始，导致每个位置会与自身比较，生成Or(Not(Q[i][j]), Not(Q[i][j]))（等价于Not(Q[i][j])），强制该位置为假，直接导致无解。

3. Q4的循环范围错误 #

原Q4的k循环范围range(min(i-1, n-j))会生成大量空约束（And([])等价于True，无实际限制），且同样存在自比较的逻辑问题。

修正后的代码 #

from z3 import *

n = 4

# 创建n×n布尔变量矩阵，(i,j)表示对应位置是否有皇后
Q = [[Bool(f"x_{i+1}_{j+1}") for j in range(n)] for i in range(n)]

# Q1：每行至少有一个皇后
Q1 = []
row_at_least_one = []
for i in range(n):
    row_vars = [Q[i][j] for j in range(n)]
    row_at_least_one.append(Or(row_vars))
Q1.append(And(row_at_least_one))

# Q2：每行最多有一个皇后（任意两位置不同时为真）
Q2 = []
for i in range(n):
    for j in range(n-1):
        row_pairs = []
        for k in range(j+1, n):
            row_pairs.append(Or(Not(Q[i][j]), Not(Q[i][k])))
        Q2.append(And(row_pairs))

# Q3：每列最多有一个皇后
Q3 = []
for j in range(n):
    for i in range(n-1):
        col_pairs = []
        for k in range(i+1, n):
            col_pairs.append(Or(Not(Q[i][j]), Not(Q[k][j])))
        Q3.append(And(col_pairs))

# Q4：左上到右下的主对角线约束（i-j为定值）
Q4 = []
for i1 in range(n):
    for j1 in range(n):
        for i2 in range(i1+1, n):
            j2 = j1 + (i2 - i1)
            if j2 < n:
                Q4.append(Or(Not(Q[i1][j1]), Not(Q[i2][j2])))

# Q5：右上到左下的副对角线约束（i+j为定值）
Q5 = []
for i1 in range(n):
    for j1 in range(n):
        for i2 in range(i1+1, n):
            j2 = j1 - (i2 - i1)
            if j2 >= 0:
                Q5.append(Or(Not(Q[i1][j1]), Not(Q[i2][j2])))

# 组合所有约束
eight_queens_c = Q1 + Q2 + Q3 + Q4 + Q5

s = Solver()
s.add(eight_queens_c)
if s.check() == sat:
    m = s.model()
    r = [[m.evaluate(Q[i][j]) for j in range(n)] for i in range(n)]
    print_matrix(r)
else:
    print("failed to solve")

修正说明 #

1. 补全对角线约束：将Q4、Q5加入最终约束列表，覆盖所有对角线的冲突检查；
2. 简化对角线逻辑：放弃原复杂循环，改用三重循环直接遍历所有对角线位置对，逻辑更清晰，避免循环范围错误；
3. 移除自比较问题：仅检查i2 > i1的位置对，彻底避免同一位置的无效约束。

内容的提问来源于stack exchange，提问作者th3man7