Wolfram Computation Meets Knowledge

Solving Knightdoku Challenges the Wolfram Way

Solving Knightdoku Challenges the Wolfram Way

Each issue of the Mathematical Association of America’s Math Horizons presents readers with puzzles to solve, and the April 2021 issue included the “Knightdoku” challenge created by David Nacin, a math professor at William Paterson University in Wayne, New Jersey.

In this puzzle, a simple Sudoku-like problem is described based on chess knights. Each cell in the 9×9 grid may contain a knight. The initial board configuration defines the placement of a set of knights that has 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 is reachable from the knight in the 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, each column and each 3×3 block must have exactly three knights.

The puzzle included two board configurations to solve: a warm-up board and a regular—that is, harder!—one. Here’s the warm-up board:

Warm-up puzzle board

© Mathematical Association of America, 2021. All rights reserved.

And here’s the regular board:

Regular puzzle board

© Mathematical Association of America, 2021. All rights reserved.

The challenge for me was not just solving Nacin’s Knightdoku puzzle but to do so using the Wolfram Language, which offers a variety of ways to solve Sudoku puzzles.

Solving a Sudoku-like Problem Based on Chess Knights

Games like Sudoku are relatively straightforward to solve using Boolean constraint solvers. In essence, you boil the problem down to relations among a set of logical variables that represent possible board configurations.

For example, if we have two cells where 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.

Helper Functions

First, we must create some helper functions for forming conjunctions and disjunctions from lists that will be useful later in building our logical expressions:

AndList
&#10005


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

First, we create a basic configuration for the warm-up board:

board1
&#10005


Then we make the regular board configuration:

board2
&#10005


For convenience, we will also create some associations for use later in looking up these initial markings when we plot the solver results:

board1assoc
&#10005


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, and that s[[i,j,2]] means there is no knight:

s = Table
&#10005


We’ll also create an association mapping coordinates to the two logical variables for that coordinate (this is mostly useful in debugging and looking at constraints):

scoords =  Association
&#10005


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 nor unmarked, or both marked and unmarked, is invalid, so we exclude them:

uniqueCellConstraint = AndList
&#10005


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, the function we created earlier, 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

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}:

neighbors
&#10005


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 1s and 2s containing the appropriate number of 1s and 2s based on the expected number of neighbors. We include the knight in the center of the neighborhood as marked (s[[x,y,1]]):

possibleNeighborConfigs
&#10005


Combining these is similar to what we did above, but with the addition of Or in the expression. Specifically, we need to And the neighbors together for each neighborhood, and join each possible neighborhood with an Or. Finally, we conjoin all of these And/Or expressions across all initial knight markings:

initialConstraints
&#10005


Board Constraints

We also need to add the generic board constraints that are similar to Sudoku: at most three knights per row, column and 3×3 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 a constraint that at most three per row can be set:

possibleRowConfigs
&#10005


rowConstraints =  AndList
&#10005


Similarly, set a constraint for at most three per column:

possibleColConfigs
&#10005


colConstraints =  AndList
&#10005


Also add a constraint for 3×3 boxes:

possibleBoxConfigs
&#10005


boxConstraints =  AndList
&#10005


Solve the System

Now we’re ready to solve both puzzle boards.

Board Configuration #1

We can solve the system using the satisfiability solver over the set of logical variables:

soln = SatisfiabilityInstances
&#10005


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 :

res = ArrayReshape
&#10005


m = Table
&#10005


Board Configuration #2

We can apply the same technique to the second, harder board provided by Nacin:

soln = SatisfiabilityInstances
&#10005


res = ArrayReshape
&#10005


m = Table
&#10005


If you’re interested in other examples of the Wolfram Language applied to Sudoku puzzles, check out posts such as “Solving Sudoku as an Integer Programming Problem” and “Using Recursion and FindInstance to Solve Sudoku” by Wolfram Community members. You can also find more interesting puzzles created by David Nacin at Quadrata, his puzzle blog.

Matthew Sottile is a computer scientist who works in the Center for Applied Scientific Computing at the Lawrence Livermore National Laboratory. His research is in the areas of programming languages, compilers and formal methods. Sottile has been an active Wolfram Mathematica user since 1995 and uses it for generative art, solving puzzles and studying rewriting and proof systems.

Visit Wolfram Community or the Wolfram Function Repository to embark on your own computational adventures!

Comments

Join the discussion

!Please enter your comment (at least 5 characters).

!Please enter your name.

!Please enter a valid email address.