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 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.