Lesson 3

The code below implements exactly all this. It also contains an additional technical detail: the function \(\texttt{varnum}\) converts a pair of indices \(0 \le i,j < n\) into a unique index from \(\{1, 2, \dotsc, n^{2}\}\).

from itertools import combinations, product
from pycosat import solve

n = 30
clauses = []


# converts a pair of integers into a unique integer
def varnum(i, j):
    assert i in range(n) and j in range(n)
    return i * n + j + 1


# each row contains at least one queen
for i in range(n):
    clauses.append([varnum(i, j) for j in range(n)])

# each row contains at most one queen
for i, (j1, j2) in product(range(n), combinations(range(n), 2)):
    clauses.append([-varnum(i, j1), -varnum(i, j2)])

# each column contains at most one queen
for j, (i1, i2) in product(range(n), combinations(range(n), 2)):
    clauses.append([-varnum(i1, j), -varnum(i2, j)])

# no two queens stay on the same diagonal
for (i1, i2), (j1, j2) in product(combinations(range(n), 2), product(range(n), repeat=2)):
    if abs(i1 - i2) == abs(j1 - j2):
        clauses.append([-varnum(i1, j1), -varnum(i2, j2)])


assignment = solve(clauses)
for i, j in product(range(n), repeat=2):
    if assignment[varnum(i, j) - 1] > 0:
        print(j, end=' ')

26 24 22 25 23 17 4 9 11 8 21 3 6 0 19 15 7 27 2 28 1 29 18 20 12 14 16 10 13 5