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:

In[]:=

ArrayPlot[SelectFirst[Permutations[IdentityMatrix[8]],NoneTrue[Subsets[Position[#,1],{2}],Apply[Total[#1]===Total[#2]||Subtract@@#1===Subtract@@#2&]]&],Mesh->True]

Out[]=

In[]:=

Export["~/git/chriswolfram.github.io/content/projects/queen-armies/8queens.svg",%]

Out[]=

~/git/chriswolfram.github.io/content/projects/queen-armies/8queens.svg

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

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 be true when a queen from army is standing on square . To express that no two queens from opposing armies occupy the same square, a constraint like this could be used

b

x,y,a

a

(x,y)

∀

x,y,a,a'

b

x,y,a

b

x,y,a'

where is a coordinate on the board, and and 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.

(x,y)

a

a'

In[]:=

AllTrue[Range[8],x|->AllTrue[Range[8],y|->AllTrue[Range[2],a|->Implies[Indexed[b,{x,y,a}],NoneTrue[Complement[Range[2],{a}],Indexed[b,{x,y,#}]&]]]]]

Out[]=

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[]:=

queenReachable[{x_,y_}, {width_,height_}]:= Select[Union[ Table[{x,j},{j,height}], Table[{i,y},{i,width}], Table[{x,y}+i,{i,1-x,width-x}], Table[{x,y}+{i,-i},{i,1-x,width-x}] ],Apply[1<=#1<=width&&1<=#2<=height&]]

In[]:=

capturingConstraints[b_, boardDims_, armyCount_] := And@@Flatten@Array[ Function[{q,x,y}, Implies[Indexed[b,{q,x,y}], AllTrue[ Flatten[Function[q2, Indexed[b,Prepend[#,q2]]&/@queenReachable[{x,y},boardDims] ]/@DeleteCases[Range[armyCount],q] ], Not ] ] ], Prepend[boardDims,armyCount]]

In[]:=

armySizeConstraints[b_, boardDims_, armyCount_, armySize_] := AllTrue[ Range[armyCount], Function[q, BooleanCountingFunction[{armySize},Times@@boardDims]@@ Flatten[Array[Indexed[b,{q,##}]&,boardDims]] ] ]

In[]:=

boardConstraints[b_, boardDims_, armyCount_, armySize_] := capturingConstraints[b, boardDims, armyCount] && armySizeConstraints[b, boardDims, armyCount, armySize]

In[]:=

boardVariables[b_, boardDims_, armyCount_] := Array[Indexed[b,{##}]&, Prepend[boardDims,armyCount]]

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.

In[]:=

processInstance[{flatInst_}, vars_] := vars /. Thread[Flatten[vars]->flatInst]processInstance[{}, vars_] := Missing[]

In[]:=

findInstance[constraints_, vars_] := processInstance[ SatisfiabilityInstances[constraints, Flatten[vars], 1, Method->"SAT"], vars ]

In[]:=

equivalentDownwardRotations[inst_] := NestWhileList[RotateRight[#,{0,1}]&, inst, !Or@@Flatten[#[[All,-1]]]&]

In[]:=

equivalentRotationsStep[inst_] := Union[ equivalentDownwardRotations[inst], Reverse[#,{2}]&/@ equivalentDownwardRotations[Reverse[inst,{2}]], Transpose[#,2<->3]&/@ equivalentDownwardRotations[Transpose[inst,2<->3]], Transpose[Reverse[#,{2}],2<->3]&/@ equivalentDownwardRotations[Reverse[Transpose[inst,2<->3],{2}]] ]

In[]:=

equivalentRotations[inst_] := FixedPoint[Union@*Catenate@*Map[equivalentRotationsStep], {inst}]

In[]:=

equivalentInstances[inst_] := Select[ Union@Catenate[ #, Reverse[#,{2}], Transpose[#,2<->3], Reverse[Transpose[#,2<->3],{2}], Transpose[Reverse[#,{2}],2<->3], Reverse[Transpose[Reverse[#,{2}],2<->3],{2}], Transpose[Reverse[Transpose[#,2<->3],{2}],2<->3], Reverse[Transpose[Reverse[Transpose[#,2<->3],{2}],2<->3],{2}] &/@Catenate[equivalentRotations/@Permutations[inst]]], Dimensions[#]===Dimensions[inst]& ]

In[]:=

instanceConstraints[inst_, vars_] := Or@@Flatten[MapThread[If[#1,Not,Identity][#2]&,{inst,vars},3],2]

### Results

Results