如何用 Z3 求解器求解 n 个皇后问题答案

【问题标题】：How to solve nqueen problem with Z3 solver如何用 Z3 求解器求解 n 个皇后问题
【发布时间】：2022-01-25 15:44:54
【问题描述】：

我写了一个公式来解决 nqueen 问题。它找到了一个解决方案，但我想找到所有解决方案，我如何将这个公式推广到所有解决方案：

from z3 import *
import time

def queens(n,all=0):
    start = time.time()
    sol = Solver()

    # q = [Int("q_%s" % (i)) for i in range(n) ] # n=100: ???s
    # q = IntVector("q", n) # this is much faster # n=100: 28.1s
    q = Array("q", IntSort(), BitVecSort(8)) # n=100: ??s

    # Domains
    sol.add([And(q[i]>=0, q[i] <= n-1) for i in range(n)])

    # Constraints
    for i in range(n):
        for j in range(i):
            sol.add(q[i] != q[j], q[i]+i != q[j]+j, q[i]-i != q[j]-j)

    if sol.check() == sat:
        mod = sol.model()
        ss = [mod.evaluate(q[i]) for i in range(n)]
        print(ss)
        # Show all solutions
        if all==1:
            num_solutions = 0
            while sol.check() == sat:
                m = sol.model()
                ss = [mod.evaluate(q[i]) for i in range(n)]
                sol.add( Or([q[i] != ss[i] for i in range(n)]) )
                print("q=",ss)
                num_solutions = num_solutions + 1

            print("num_solutions:", num_solutions)
    else:
        print("failed to solve")

    end = time.time()
    value = end - start
    print("Time: ", value)


for n in [8,10,12,20,50,100,200]:
    print("Testing ", n)
    queens(n,0)

对于 N=4，我尝试展示 2 个解决方案

对于 N=8，我尝试显示所有 92 个解决方案

【问题讨论】：

标签： z3 n-queens

【解决方案1】：

您的大部分内容都是正确的，尽管您对 find-all-solutions 部分的编码方式存在问题。 Z3 教程附带的 N-queens 解决方案在这里：https://ericpony.github.io/z3py-tutorial/guide-examples.htm

您可以将其变成“查找所有解决方案”的版本，如下所示：

from z3 import *

def queens(n):
    Q = [Int('Q_%i' % (i + 1)) for i in range(n)]

    val_c  = [And(1 <= Q[i], Q[i] <= n) for i in range(n)]
    col_c  = [Distinct(Q)]
    diag_c = [If(i == j, True, And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)) for i in range(n) for j in range(i)]

    sol = Solver()
    sol.add(val_c + col_c + diag_c)

    num_solutions = 0

    while sol.check() == sat:
        mod = sol.model()
        ss = [mod.evaluate(Q[i]) for i in range(n)]
        print(ss)
        num_solutions += 1
        sol.add(Or([Q[i] != ss[i] for i in range(n)]))

    print("num_solutions:", num_solutions)

queens(4)
queens(8)

这将为N=4 打印2 个解决方案，为N=8 打印92 个解决方案。

【讨论】：