Continuing the series of solving puzzles using an integer SMT solver we look now at the Suguru puzzle. This popular number placement puzzle is published in the Daily Mail newspaper and other publications. The puzzle offers a variable size rectangular grid sub-divided into regions into which sequential numbers ( 1.. region size) must be placed. Some initial clue numbers are provided. The numbers must be unique within the regions and each cell must not touch (kings move) any other cell with the same value.
 |
| Suguru puzzle 6 by 6 |
Encoding
The puzzle is encoded into text then a script is used to generate the underlying logic of the puzzle. These logic lines are then passed to an SMT solver for analysis and resolution. Microsoft's Z3 and MathSAT solvers are used. A region letter is used for each cell followed by a clue number if provided.
#Suguru Page59 DR su_002.txt
a,b,b,b,b,c
a,a4,d,c3,c,c
a,d,d,d,e5,c
f,f2,d,g,e,e
h,f,g,g,g,e2
h,f,f,g,i,e
Puzzle Logic
The logic of the puzzle breaks down in to two main sets of constraints. Firstly the regions have to have ascending numbers and secondly adjoining cell values must differ. Some clue numbers are provided. A single cell region must have the value 1 see above ( region i, the fifth cell along the bottom row ).
This puzzle resembles Hidato for a neighbour cell constraints and KenKen for the region values constraints.
After the usual preamble an Int variable is set for each cell
(set-logic UFNIA)
(set-option :produce-models true)
(set-option :produce-assignments true)
(declare-const V0 Int)
(declare-const V1 Int)
(declare-const V2 Int)
.... up to cell V35
(declare-const V35 Int)
As the region sizes have been analysed during input we can set constrains for each cell based on the number of cells in the region.
(assert (and (>= V0 1) (<= V0 4)))
(assert (and (>= V1 1) (<= V1 4)))
(assert (and (>= V2 1) (<= V2 4)))
(assert (and (>= V3 1) (<= V3 4)))
(assert (and (>= V4 1) (<= V4 4)))
(assert (and (>= V5 1) (<= V5 5))) ; Region c
(assert (and (>= V6 1) (<= V6 4)))
.... up to cell V35
The clue numbers are set ....
(assert (= V7 4 ))
(assert (= V9 3 ))
(assert (= V16 5 ))
(assert (= V19 2 ))
(assert (= V29 2 ))
The region numbers are set .... to be distinct values ..
(assert (distinct V0 V6 V7 V12)) ; Region a
(assert (distinct V1 V2 V3 V4)) ; Region b
(assert (distinct V5 V9 V10 V11 V17)) ; Region c
(assert (distinct V8 V13 V14 V15 V20)) ; Region d
(assert (distinct V16 V22 V23 V29 V35)) ; Region e
(assert (distinct V18 V19 V25 V31 V32)) ; Region f
(assert (distinct V21 V26 V27 V28 V33)) ; Region g
(assert (distinct V24 V30)) ; Region h
Except for single cell region that is just set to a clue number 1.
(assert (= V34 1)); Region i Single cell
Neighbour cells
Finding the neighbours for each cell is the interesting part for this puzzle. Sequential cell numbers are used and the width (w) of the puzzle is known. In the centre of the puzzle, for the clue in cell 9 we can find its neighbours by +/- w and +/- 1.
The following are the addresses of the neighbours of cell 9
[ 9 -w -1 ] [ 9 -w ] [ 9 -w +1] [9 -1] [9+1] [ 9 +w -1 ] [ 9 -w ] [ 9 +w +1]
 |
| Suguru Grid size 6 Neighbours of 9 |
giving cell numbers 2,3,4,8,10,14,15,16 and producing the the logic line
(assert (and
(not (= V9 V2)) (not (= V9 V3)) (not (= V9 V4))
(not (= V9 V8)) (not (= V9 V10))
(not (= V9 V14)) (not (= V9 V15)) (not (= V9 V16)
))); Neighbours of 9
However for the cells along the edges and in the corner of the puzzle the neighbour cell generation has to avoid falling of the edge of the puzzle. Also sequential cells are not necessarily neighbours see cell 11 is not a neighbour of cell 12. The corners only have 3 neighbours and cells along the side only 5 neighbours.
To find the correct neighbours of a cell we calculate all the possible neighbours then filter out the non-neighbour and off the edge cells.
@nlist = ( $cell-1-$w, $cell-0-$w, $cell+1-$w, $cell-1,$cell+1,
$cell-1+$w, $cell-0+$w, $cell+1+$w );
foreach $i ( @nlist )
{ $res .= "V$i "
unless ( ( $i < 0 ) or ( $i > $last) or
( abs( $i % $w - $cell % $w ) > 1 ) )
};
The unless clause here has the key tests, first cells address below 0 and cells beyond the last possible address are excluded then critically the absolute column distance between the cells is checked. The modulus operator % gives the remainder after dividing the cell addresses in $i and $cell by the width of the board in $w. The abs function flips -ve numbers positive. If the subtraction result is more than 1 then the cells are not neighbours. Trying this on cell 11 with cells 10 and 12. For cell 10 we get abs( 11 % 6 - 10 % 6 ) = abs ( 5 - 4 ) = 1 therefore cell 10 is a neighbour of 11. For cell 12 we get abs( 11 % 6 - 12 % 6 ) = abs( 5 - 0 ) = 5 therefore cell 12 is not a neighbour of 11.
All the cell neighbours are calculated in the same way resulting in the logic lines for cell neighbour constraints.
(assert (and (not (= V0 V1)) (not (= V0 V6)) (not (= V0 V7)))); Neighbours of 0
(assert (and (not (= V1 V0)) (not (= V1 V2)) (not (= V1 V6))
(not (= V1 V7)) (not (= V1 V8)))); Neighbours of 1
........
(assert (and (not (= V6 V0)) (not (= V6 V1)) (not (= V6 V7))
(not (= V6 V12)) (not (= V6 V13)))); Neighbours of 6
........
(assert (and (not (= V8 V1)) (not (= V8 V2)) (not (= V8 V3)) (not (= V8 V7)) (not (= V8 V9)) (not (= V8 V13)) (not (= V8 V14)) (not (= V8 V15)))); Neighbours of 8
This is the more mundane approach of finding neighbour cells. In other puzzles eg Hidato a grid bigger than the game board is used with off edge cells being neutral.
Results
As with the previous puzzles the logic generating script was coded to read in the solvers output and then generate output using the original puzzle and check the answers provided. Using display colours helps identify the cells of a region.
 |
| Suguru completed showing regions and values with result check lines |
Error checks test
If another puzzle is taken and the results from the solver adjusted before display the error checks should show that cell 7 has a duplicate value.
$ perl ./suguru_smt2.pl < su_001.txt | ../solver_m5 | sed '/V7/s/4/3/' | ./suguru_smt2.pl -f su_001.txt > su_001BROKEN.html
 |
| Suguru showing error detection for cells 3,7,8 and region b |
Appendix Script Usage
A script is used to generate the logic lines from the encoded puzzle and subsequently read the solver output and generate the results display.
Usage: Suguru {options} < puzzle.txt or
Suguru {options} -f puzzle.txt < SolverOutput
-v N :Be verbose to level N ( use v=1 for detailed output )
-f puzzle.txt :Puzzle file needed when reading Solver output use STDIN otherwise
Programs reads STDIN looking for either puzzleFile format lines or Solver output lines
If the input is in puzzleFile format the program will generate solver input lines.
If the input is in Solver output lines format the program will expect a -f puzzleFile paremeter.
Using both these input streams program will then generate display .html output.
Game Rules
Each regions has cells set from 1 .. N where N is size of region. Repeats NOT allowed in any region.
Encoding Rules
Each cell belongs to a single region/cage. Regions must be uniquely filled with 1..N.
No bordering cells (kings move) can have the same number. Clue numbers are pre-place in some cells.
Single empty cell regions are 1.
Region names must be unique.
Typically puzzles are square and have 5 or 6 cells but not neccessarly
Numbers may not repeat with a region or on adjcent cells.
Each Suguru puzzle Input as follows each caged squares must belong to a region
region_lable{Value}{operation+-*/}
su_001.txt
#Suguru Number 60 DR su_001.txt
a,a,b,c,c
a,b,b,b,c2
a2,d5,c,e1,c
a,d,e,e,c
d,d,d,e4,e
to generate an SMT2 input file. Use a .. z and A .. Z or aa .. zz for region/cage names
OR Process results from solver in the following format
sat
( (V0 9)
(V1 7)
(V2 5)
(V3 3)
....
to generate an html table as output
No comments:
Post a Comment