Background

Parade magazine, a filler in the local Sunday newspaper, contains a Numbrix puzzle, the object of which is to find a serpentine path of consecutive integers, 1 through 81, through a nine by nine grid.  The puzzle typically specifies the content of every other border cell.

The Maple Logic  package has a procedure, Satisfy , that can be used to solve this puzzle.  Satisfy is a SAT-solver; given a boolean expression it attempts to find a set of equations of the form , where  are the boolean variables in the given expression and  are boolean values (true or false) that satisfy the expression (cause it to evaluate true).

A general technique to solve this and other puzzles with Satisfy is to select boolean-values variables that encode the state of the puzzle (a trial solution, whether valid or not), generate a boolean-expression of these variables that is satisfied (true) if and only if the variables are given values that correspond to a solution, pass this expression to Satisfy, then translate the returned set of boolean values (if any) to the puzzle solution.

Setup

Assign a matrix that defines the grid and the initial position.  Use zeros to indicate the cells that need values. To make it easy to inspect the expressions, a small 2 x 3 matrix is used for this demo---a full size example is given at the end.

Extract the dimensions of the Matrix

Boolean Variables

Let the boolean variable x[i,j,k] mean that cell (i,j) has value k. For example, x[2,3,6] is true when cell (2,3) contains 6, otherwise it is false. There are  boolean variables.

Initial Position

The initial position can be expressed as the following and-clause.

Adjacent Cells

The requirement that an interior cell with value k is adjacent to the cell with value k+1 can be expressed as the implication
   

   x[i,j,k] &implies &or(x[i-1,j,k+1], x[i+1,j,k+1], x[i,j-1,k+1], x[i,j+1,k+1])

Extending this to handle all cells results in the following boolean expression.

All Values Used

The following expression is true when each integer , from 1 to , is assigned to one or more cells.

Single Value

The following expression is satisfied when each cell has no more than one value.

Solution

Combine the boolean expressions into a a single and-clause and pass it to Satisfy.

Select the equations whose right size is true

Extract the lhs of the true equations

Extract the result from the indices of the vars and assign to a new Matrix

Procedure

We can now combine the manual steps into a procedure that takes an initialized Matrix and fills in a solution.

Example

Create the initial position for a 9 x 9 Numbrix and solve it.