Chess Queen Armies With SAT Solvers

September, 2022

Source notebook available here. Inspired by a post by Sander Huisman.

The eight queens puzzle is a classic chess problem. The goal is to place eight queens on a chess board so that no two can attack each other. For example:

There is an extension of the eight queens puzzle with the goal of placing opposing "armies" of queens such that no two queens from opposing armies can attack each other. However, queens from the same army are allowed to attach each other.

I saw this in a post which linked to a Rosetta Code page with solvers written in dozens of languages. However, almost all of these solvers worked in fundamentally the same way using a recursive backtracking algorithm. This is fine, but it seemed like this could also be easily done with a SAT solver, which has some performance advantages, as well as making it easier to find all possible solutions (as opposed to a single solution).

The first step in feeding this problem to a SAT solver is to represent it in the language of logic.

Compiling to Logic

The input to a SAT solver is a boolean expression which evaluates to true on a valid solution. In this case, the boolean expression will have a variable for each army for each position in the game board.

In particular, let \(b_{x,y,a}\) be true when a queen from army \(a\) is standing on square \((x,y)\). To express that no two queens from opposing armies occupy the same square, a constraint like this could be used $$\forall x,y,a,a' \quad (b_{x,y,a} \land a \neq a') \implies \neg b_{x,y,a'}$$ where \((x,y)\) is a coordinate on the board, and \(a\) and \(a'\) are opposing armies. For the actual input to the SAT solver, a universal quantifier like this is expanded into a huge number of statements of propositional logic for each case. $$\begin{align} b_{1,1,1} &\implies \neg b_{1,1,2} \\ b_{1,1,2} &\implies \neg b_{1,1,1} \\ b_{1,2,1} &\implies \neg b_{1,2,2} \\ b_{1,2,2} &\implies \neg b_{1,2,1} \\ \dots \end{align}$$ SAT solvers are designed to take huge inputs like this, so it isn't a problem.

In the full implementation, this style of constraint is used to enforce the capturing rules and boolean counting functions are used to enforce to total number of queens in each army.

In order to find multiple solutions, the previous solution can be represented in logic, negated and appended to the list of constraints. However, this leads to tons of isomorphic cases (for example, where the patterns are the same but the armies are swapped, or where the board is rotated, etc.) To solve this, all solutions isomorphic to the previous solution can be negated and appended to the list of constraints, so no more isomorphic solutions are allowed.

Results

Using this method, the SAT solver finds all three unique (up to isometry) solutions on a \(5 \times 5\) board with two armies of size four, in a fraction of a second:

There are only three unique solutions on the \(5 \times 5\) board, but there are 10 unique solutions on a \(4 \times 4\) board:

I used size four armies on the \(5 \times 5\) board and size two armies on the \(4 \times 4\) board because those are the maximal army sizes the have solutions.

I've computed all possible solutions with maximal army sizes for all board sizes from \(3 \times 2\) (the smallest size with solutions) to \(8 \times 8\). You can see all of them by picking form the menu below.