Effective Problem Solving using SAT Solvers

"...it is a constant source of annoyance when you come up with a clever special algorithm which then gets beat by translation to SAT." –Chris Jefferson

SAT solvers are programs that can solve the satisfiability problem from Boolean logic. Given a logical expression, they determine if the expression can be made true.

For example,

$$ \lnot x \rightarrow (y\lor z) $$

can be made true by setting $x$ to false, $y$ to true, and $z$ to false.

Solving $n$-Queens using a SAT solver in SageMath

The $n$-queens problem is place $n$ queens on an $n\times n$ chessboard so that no two queens attack each other.

# Initialize the solver
solver = SAT()
# Size of board
n = 8

Boolean variables

Let $Q_{i,j}$ denote that square $(i,j)$ contains a queen.

# Q[i,j] will denote there is a queen on square (i,j) 
Q = [[0 for j in range(n)] for i in range(n)]

Give each square a unique index:

$$ \begin{bmatrix} 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ 9 & 10 & 11 & 12 & 13 & 14 & 15 & 16 \\ 17&18&19&20&21&22&23&24\\ 25&26&27&28&29&30&31&32\\ 33&34&35&36&37&38&39&40\\ 41&42&43&44&45&46&47&48\\ 49&50&51&52&53&54&55&56\\ 57&58&59&60&61&62&63&64 \end{bmatrix} $$

# Give each variable a unique label in {1,...,n^2}
c = 1
for i in range(n):
    for j in range(n):
        Q[i][j] = c
        c += 1

Useful functions

# varsInCol returns the set of variables in the same column as y
def varsInCol(y):
    return {Q[i][y] for i in range(n)}

# varsInRow returns the set of variables in the same row as x
def varsInRow(x):
    return {Q[x][i] for i in range(n)}

# varsInDiag returns the set of variables in the same diagonal as (x,y)
def varsInDiag(x, y):
    diagVars = {Q[x][y]}
    for i in range(n):
        if x+i in range(n) and y+i in range(n):
            diagVars.add(Q[x+i][y+i])
        if x-i in range(n) and y-i in range(n):
            diagVars.add(Q[x-i][y-i])
    return diagVars

# varsinAntiDiag returns the set of variables in the same anti-diagonal as (x,y)
def varsInAntiDiag(x, y):
    antiDiagVars = {Q[x][y]}
    for i in range(n):
        if x+i in range(n) and y-i in range(n):
            antiDiagVars.add(Q[x+i][y-i])
        if x-i in range(n) and y+i in range(n):
            antiDiagVars.add(Q[x-i][y+i])
    return antiDiagVars

# attackedVars returns the set of variables attacked by a queen at (x,y)
def attackedVars(x, y):
    s = varsInRow(x)
    s.update(varsInCol(y))
    s.update(varsInDiag(x, y))
    s.update(varsInAntiDiag(x, y))
    s.remove(Q[x][y])
    return s

Logical constraints

There must be a queen in row 0:

$$ Q_{0,0}\lor Q_{0,1} \lor Q_{0,2} \lor Q_{0,3} \lor Q_{0,4} \lor Q_{0,5} \lor Q_{0,6} \lor Q_{0,7} $$

# There must be a queen in each row and column
for i in range(n):
    solver.add_clause(varsInRow(i))
    solver.add_clause(varsInCol(i))

If there is a queen on square (0,0), then there cannot be a queen on any square attackable by (0,0) such as (1,1):

$$ Q_{0,0} \rightarrow \lnot Q_{1,1} $$

This is logically equivalent to

$$ \lnot Q_{0,0} \lor \lnot Q_{1,1} $$

# No two queens can attack each other
for i in range(n):
    for j in range(n):
        for attacked in attackedVars(i, j):
            solver.add_clause([-Q[i][j], -attacked])

Finding a satisfying assignment

# Find a satisfying assignment of the generated instance
sat_assignment = solver()

for i in range(n):
    s = ""
    for j in range(n):
        if sat_assignment[j*n+i+1] == True:
            s += "Q"
        else:
            s += "."
    print(s)