Solving a puzzle from MAA “Math Horizons” Magazine, Volume XXVIII, Issue 4 (April 2021) by David Nacin
Solving a puzzle from MAA “Math Horizons” Magazine, Volume XXVIII, Issue 4 (April 2021) by David Nacin
Puzzle page can be found here
Games like Sudoku are relatively straightforward to solve using Boolean constraint solvers. In essence, you boil the problem down to relations amongst a set of logical variables that represent possible board configurations. For example, if we have two cells that we want to make one true and the other false, we can create four variables: two for the first cell (cell1false, cell1true), and two for the second cell (cell2false, cell2true). A valid configuration would satisfy the constraint (cell1false and cell2true) or (cell1true and cell2false). This logical expression ((cell1false&&cell2true)||(cell1true&&cell2false)) can be handed to a satisfiability solver to determine if a configuration exists that satisfies the logical constraints.
In this puzzle from MAA Math Horizons magazine, a simple Sudoku-like problem is described based on chess knights. Each cell in the 9x9 grid may contain a chess knight. The initial board configuration defines the placement of a set of knights that have a specific number of knights that must be present in their neighborhood in the solution. The neighborhood of a knight is the set of cells that are reachable from the knight in one L-shaped chess move that knights are allowed to make.
In addition to the initial placement of knights, a valid solution must obey a Sudoku-like constraint. Specifically, each row must have exactly 3 knights, each column must have exactly 3 knights, and each 3x3 block must have exactly 3 knights.
Helper functions
Helper functions
First we establish some helper functions for forming conjunctions and disjunctions from lists. These are useful in building our logical expressions later.
In[]:=
AndList[l_]:=Fold[And,True,l];OrList[l_]:=Fold[Or,False,l];
Board configuration :
Board configuration :
Initial board configuration is a list of triples: {x,y,n} where {x,y} is the position on the board (using 1-based indices), and n is the number of neighbors the knight at {x,y} that contain a knight in the solution. A neighbor is defined as a cell reachable via a legal knight move.
The article provides two examples - a basic configuration:
In[]:=
board1={{1,9,0},{2,2,2},{3,4,3},{4,2,1},{4,3,4},{5,2,6},{5,5,4},{5,8,0},{6,7,3},{6,8,2},{7,6,5},{8,8,2},{9,1,0}};
A regular (harder) configuration is also provided:
In[]:=
board2={{1,7,1},{2,6,1},{3,2,0},{4,8,2},{4,9,2},{5,4,1},{5,5,2},{5,6,4},{6,1,1},{6,2,2},{7,8,1},{8,4,0},{9,3,1}};
For convenience, we will also create some associations for use later in looking up these initial markings when we plot the solver results:
In[]:=
board1assoc=Association[({#[[1]],#[[2]]}->#[[3]])&/@board1];board2assoc=Association[({#[[1]],#[[2]]}->#[[3]])&/@board2];
Defining logical variables :
Defining logical variables :
We need to encode the state of the board via logical variables, so we define a set of Boolean values for the possible states of each cell (has a knight, has no knight). We use the convention that s[[i,j,1]] means {i,j} has a knight, s[[i,j,2]] means no knight.
In[]:=
s=Table[Table[Table[Unique[svar],{z,1,2}],{y,1,9}],{x,1,9}];
For convenience, we’ll create an association mapping coordinates to the two logical variables for that coordinate. This is mostly useful in debugging and looking at constraints.
In[]:=
scoords=Association[Table[Table[{s[[i,j,1]]->{i,j,1},s[[i,j,2]]->{i,j,2}},{i,1,9}],{j,1,9}]//Flatten[#,2]&];
The first logical constraint we establish is necessary to guarantee that a cell is either marked or unmarked. Having a cell that is neither marked or unmarked, or both marked and unmarked, is invalid so we exclude them.
In[]:=
uniqueCellConstraint=AndList[AndList/@Table[Table[(s[[i,j,1]]&&Not[s[[i,j,2]]])||(Not[s[[i,j,1]]]&&s[[i,j,2]]),{i,1,9}],{j,1,9}]];
Most of the code we write for constraints looks like this. In this case, the innermost tables set up a per-cell constraint. We then map AndList over the table to form a conjunction from the columns of each row of the table, and then apply AndList one more time to conjoin the rows into one large logical expression.
Neighborhood constraints :
Neighborhood constraints :
For our initial configuration, we need to consider the cells that are reachable from each knight obeying the boundaries of the board. We can write a simple function that enumerates the coordinates of the neighbors of a cell {x,y}.
In[]:=
neighbors[{x_,y_}]:=Select[{{x-1,y-2},{x-1,y+2},{x-2,y-1},{x-2,y+1},{x+1,y-2},{x+1,y+2},{x+2,y-1},{x+2,y+1}},(#[[1]]>0&&#[[1]]<10&&#[[2]]>0&&#[[2]]<10)&];
For a given position and number of expected knight neighbors, generate all possible valid assignments. We achieve this by taking the set of neighbors and associating with each a value of 1 or 2. The order of 1 and 2 assignments is achieved by calculating all permutations of a sequence of 1’s and 2’s containing the appropriate number of 1’s and 2’s based on the expected number of neighbors. We include the knight in the center of the neighborhood as marked (s[[x,y,1]]).
In[]:=
possibleNeighborConfigs[{x_,y_,n_}]:=Module[{ns,perms},ns=neighbors[{x,y}];perms=Permutations[Join[Table[1,{i,1,n}],Table[2,{i,1,Length[ns]-n}]]];Table[Join[(*containsaknight*){s[[x,y,1]]},(*neighborpossibilities*)Table[s[[ns[[j,1]],ns[[j,2]],perms[[i,j]]]],{j,1,Length[ns]}]],{i,1,Length[perms]}]]
Combining these is similar to what we did above, but with an addition of Or’s in the expression. Specifically, we need to And the neighbors together for each neighborhood, and join each possible neighborhood with Or’s. Finally, we conjoin all of these And/Or expressions across all initial knight markings.
In[]:=
initialConstraints[board_]:=AndList[OrList[AndList/@possibleNeighborConfigs[#]]&/@board];
Board constraints :
Board constraints :
We also need to add the generic board constraints that are similar to Sudoku: at most three knights per row, per column, and per 3x3 block. These follow the same pattern as above: we create all permutations of marked/unmarked for each row, column, and block and join them with And and Or operators.
Add constraint that at most 3 per row can be set.
In[]:=
possibleRowConfigs[r_]:=Module[{ns,perms},ns=Table[{i,r},{i,1,9}];perms=Permutations[{1,1,1,2,2,2,2,2,2}];Table[Table[s[[ns[[j,1]],ns[[j,2]],perms[[i,j]]]],{j,1,Length[ns]}],{i,1,Length[perms]}]]
In[]:=
rowConstraints=AndList[Table[OrList[AndList/@possibleRowConfigs[i]],{i,1,9}]];
Similarly set constraint for at most 3 per column.
In[]:=
possibleColConfigs[c_]:=Module[{ns,perms},ns=Table[{c,i},{i,1,9}];perms=Permutations[{1,1,1,2,2,2,2,2,2}];Table[Table[s[[ns[[j,1]],ns[[j,2]],perms[[i,j]]]],{j,1,Length[ns]}],{i,1,Length[perms]}]]
In[]:=
colConstraints=AndList[Table[OrList[AndList/@possibleColConfigs[i]],{i,1,9}]];
Also add constraint for 3x3 boxes.
In[]:=
possibleBoxConfigs[{bx_,by_}]:=Module[{ns,perms},ns=Table[Table[{i+((bx-1)*3),j+((by-1)*3)},{j,1,3}],{i,1,3}]//Flatten[#,1]&;perms=Permutations[{1,1,1,2,2,2,2,2,2}];Table[Table[s[[ns[[j,1]],ns[[j,2]],perms[[i,j]]]],{j,1,Length[ns]}],{i,1,Length[perms]}]]
In[]:=
boxConstraints=AndList[OrList[AndList/@possibleBoxConfigs[#]]&/@Flatten[Table[Table[{i,j},{i,1,3}],{j,1,3}],1]];
Solve the system
Solve the system
First board:
First board:
Now we can solve the system using the satisfiability solver over the set of logical variables:
In[]:=
soln=SatisfiabilityInstances[boxConstraints&&rowConstraints&&colConstraints&&initialConstraints[board1]&&uniqueCellConstraint,Flatten[s]];
For visualization, we reshape the result to determine what the assignment was to each logical variable in the same shape as the board. We indicate the original knights as ♞ with a superscript indicating the number of neighbors it must have. The knights that were filled in by the solver are indicated as ♘.
Second board:
Second board:
We can apply the same technique to the second board configuration provided by the article author.