How to solve nqueen problem with Z3 solver

Question

I write a formula to solve nqueen problem. It finds one of the solution but I want find all solution how I generalize to all solution for this formula:

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)

For N=4 I try to show 2 solution

For N=8 I try to show all 92 solution

Answer 1

You got most of it correct, though there are issues with how you coded the find-all-solutions part. There's a solution for N-queens that comes with the z3 tutorial here: https://ericpony.github.io/z3py-tutorial/guide-examples.htm

You can turn it into an "find-all-solutions" versions like this:

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)

This'll print 2 solutions for N=4 and 92 for N=8.