Lesson 2

Let's write a program that takes as input a number \(n \in \mathbb{Z}_{>0}\) and places \(n\) (mutually non-attacking) queens on an \(n \times n\) board using a SAT-solver.

We introduce \(n^{2}\) Boolean variables: for \(0 \le i, j < n\), the variable \(x_{ij}\) equals one if and only if there is a queen in cell \((i,j)\). To guarantee that the placement is correct, we add the following constraints:

• For each \(0 \le i < n\), there is at least one queen in row \(i\): \[(x_{i0}\lor x_{i1}\lor\dotsb \lor x_{i(n-1)}) \ .\] This guarantees that there are at least \(n\) queens on the board.


• For each \(0 \le i < n\), there is no more than one queen in row \(i\). To write this in CNF, for all \(0 \le j_{1} \neq j_{2} < n\) add a clause \[(\overline{x_{ij_1}}\lor \overline{x_{ij_2}}) \ .\] This guarantees that there are at most \(n\) queens. Together with the previous constraint, we get that there are exactly \(n\) queens.


• For each \(0 \le j < n\), in the \(j\)-th column there is at most one queen: for all \(0 \le i_{1} \neq i_{2} < n\), add a clause \[(\overline{x_{i_1j}}\lor \overline{x_{i_2j}}) \ .\] Actually, we could just write that each column must have at least one queen. Since we already know there are exactly \(n\) queens, two queens cannot end up in the same column. Nevertheless, practice shows that these 2-clauses make the SAT-solver’s life easier. Roughly speaking, these 2-clauses allow the SAT-solver immediately after assigning \(x_{ij}=1\) to set \(x_{i'j}=0\) for all \(i' \neq i\), instead of deducing it somehow.


• Finally, we need to forbid two queens from being on the same diagonal. We'll do this naively for now: for each pair of cells \((i_{1},j_{1})\) and \((i_{2},j_{2})\) on the same diagonal (\(|i_{1}-i_{2}|=|j_{1}-j_{2}|\)), add a clause \[(\overline{x_{i_1j_1}}\lor \overline{x_{i_2j_2}}) \ .\]