:

Solving a Numbrix Puzzle with Logic

Maple

Solving a Numbrix Puzzle with Logic

 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.

 > M := Matrix(2,3, {(1,1) = 1, (1,3) = 5});
 (2.1)

Extract the dimensions of the Matrix

 > (m,n) := upperbound(M);
 (2.2)
 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.

 > initial := &and(seq(seq(ifelse(M[i,j] = 0, NULL, x[i,j,M[i,j]]), i = 1..m), j = 1..n));
 (4.1)

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.

 > adjacent := &and(seq(seq(seq(          x[i,j,k] &implies &or(NULL                                , ifelse(1
 (5.1)

All Values Used

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

 > allvals := &and(seq(seq(&or(seq(x[i,j,k], k=1..m*n)), i=1..m), j=1..n));
 (6.1)

Single Value

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

 > single := ¬ &or(seq(seq(seq(seq(x[i,j,k] &and x[i,j,kk], kk = k+1..m*n), k = 1..m*n-1), i = 1..m), j = 1..n));
 (7.1)

Solution

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

 > sol := Logic:-Satisfy(&and(initial, adjacent, allvals, single));
 (8.1)

Select the equations whose right size is true

 > sol := select(rhs, sol);
 (8.2)

Extract the lhs of the true equations

 > vars := map(lhs, sol);
 (8.3)

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

 > S := Matrix(m,n):
 > for v in vars do S[op(1..2,v)] := op(3,v); end do:
 > S;
 (8.4)
 Procedure We can now combine the manual steps into a procedure that takes an initialized Matrix and fills in a solution. Numbrix := proc( M :: ~Matrix, { inline :: truefalse := false } )

Example

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

 > P := Matrix(9, {(1,1)=11, (1,3)=7, (1,5)=3, (1,7)=81, (1,9)=77, (3,9)=75, (5,9)=65, (7,9)=55, (9,9)=53                , (9,7)=47, (9,5)=41, (9,3)=39, (9,1)=37, (7,1)=21, (5,1)=17, (3,1)=13});
 (10.1)
 > CodeTools:-Usage(Numbrix(P));
 memory used=0.77GiB, alloc change=220.03MiB, cpu time=15.55s, real time=12.78s, gc time=3.85s
 (10.2)
 >

numbrix.mw

﻿