Solving Hidato and Knights tour using an SMT (integer) solver

Continuing the series of solving puzzles using an integer SMT solver we look now at the Hidato puzzle. This popular integer placement puzzle is published in the Daily Mail newspaper and other publications. The puzzle offers a variable size and shaped grid of interconnected boxes into which sequential numbers must be placed. Some initial clue numbers are provided to guide placement. The sequential numbers must be traceable on the finished grid by moving 1 step in any direction (kings move). No edge wraparound or box hopping is allowed.

The puzzle is simply encoded into text then a script is used to generate the underlying logic of the puzzle. These logic lines are passed to an SMT solver for analysis and resolution. Microsoft's Z3 and MathSAT solvers are used.

#Hidato dm unk hi_002.txt

x,x,0,0,10,0

x,0,14,12,0,9,0

0,16,x,x,0,1,0,0

17,0,x,0,23,0,0,4

30,0,0,0,26,x,45,0

0,0,0,0,x,x,0,46

x,0,28,0,0,40,0

x,x,0,37,38,39

An x is used to pad the left hand edge and for interior blocks. 

From a logical point of view this puzzle most resembles the Gogen letter placement puzzle and will be tackled in a similar way. 

The choice is to have either the puzzle solve for the values in the answer squares or solve for the position of the step numbers on the grid. The clues can interpreted either as "square 38 is step 1" or "step 1 is on square 38".  When reviewing the possible solution values (step X is on square number Y) form a chain of increasing X step values we can generate extra solving logic. The steps of the puzzle force a relationship between nearby squares.

Whereas using square numbers and trying to find the step number for that square is not useful due to the differing positional relationship of sequential squares. 

Generating a variable for each of the step number 1 to 46 ( for this puzzle). The position squares on the puzzle are numbered from 1 in to top left to 128 on the bottom right. The results values will forced into the available answer squares position ranges. The technique of adding padding squares to the right hand side is used to help with the generation of the "must be next to constraint". 

Hidato position numbers for this puzzle

After some preamble to set the solver into linear integer mode the results variables are declared. 

(set-logic LIA)

(set-option :produce-models true)

(set-option :produce-assignments true)

(declare-const V1 Int)

(declare-const V2 Int)

(declare-const V3 Int)

(declare-const V4 Int)

....

(declare-const V46 Int)

Next we insure that every number has a unique position.

(assert (distinct V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46  ))

Then the clue number known placements are set. Clue number 10 is in position 5, clue 14 position 19 etc.

(assert (= V10 5))

(assert (= V14 19))

(assert (= V12 20))

(assert (= V9 22))

(assert (= V16 34))

......

(assert (= V39 118))

Next we block out the un-fillable positions ( marked in red) using a line for each of the variables. Positions 1,2,7,8,17,24 35,36 etc are all individually blocked out 

(assert (and 

(not (= 1 V1)) (not (= 1 V2)) (not (= 1 V3)) 

(not (= 1 V4)) (not (= 1 V5)) (not (= 1 V6)) (not (= 1 V7)) 

(not (= 1 V8)) (not (= 1 V9)) (not (= 1 V10)) (not (= 1 V11)) 

(not (= 1 V12)) (not (= 1 V13)) (not (= 1 V14)) (not (= 1 V15)) 

(not (= 1 V16)) (not (= 1 V17)) (not (= 1 V18)) (not (= 1 V19)) 

(not (= 1 V20)) (not (= 1 V21)) (not (= 1 V22)) (not (= 1 V23)) 

(not (= 1 V24)) (not (= 1 V25)) (not (= 1 V26)) (not (= 1 V27)) 

(not (= 1 V28)) (not (= 1 V29)) (not (= 1 V30)) (not (= 1 V31)) 

(not (= 1 V32)) (not (= 1 V33)) (not (= 1 V34)) (not (= 1 V35)) 

(not (= 1 V36)) (not (= 1 V37)) (not (= 1 V38)) (not (= 1 V39)) 

(not (= 1 V40)) (not (= 1 V41)) (not (= 1 V42)) (not (= 1 V43)) 

(not (= 1 V44)) (not (= 1 V45)) 

 )) ; block 1

...... 

(assert (and (not (= 120 V1)) (not (= 120 V2)) (not (= 120 V3)) (not (= 120 V4)) (not (= 120 V5)) (not (= 120 V6)) (not (= 120 V7)) (not (= 120 V8)) (not (= 120 V9)) (not (= 120 V10)) (not (= 120 V11)) (not (= 120 V12)) (not (= 120 V13)) (not (= 120 V14)) (not (= 120 V15)) (not (= 120 V16)) (not (= 120 V17)) (not (= 120 V18)) (not (= 120 V19)) (not (= 120 V20)) (not (= 120 V21)) (not (= 120 V22)) (not (= 120 V23)) (not (= 120 V24)) (not (= 120 V25)) (not (= 120 V26)) (not (= 120 V27)) (not (= 120 V28)) (not (= 120 V29)) (not (= 120 V30)) (not (= 120 V31)) (not (= 120 V32)) (not (= 120 V33)) (not (= 120 V34)) (not (= 120 V35)) (not (= 120 V36)) (not (= 120 V37)) (not (= 120 V38)) (not (= 120 V39)) (not (= 120 V40)) (not (= 120 V41)) (not (= 120 V42)) (not (= 120 V43)) (not (= 120 V44)) (not (= 120 V45)) )) ; block 120

The allowable columns ranges are set for row for each variable. Ranges 1..8 , 17..24, 33..40 etc.

(assert ( or 

(and (> V1 0 )  (< V1 9))   (and (> V1 16 )  (< V1 25)) 

(and (> V1 32 ) (< V1 41))  (and (> V1 48 )  (< V1 57)) 

(and (> V1 64 ) (< V1 73))  (and (> V1 80 )  (< V1 89)) 

(and (> V1 96 ) (< V1 105)) (and (> V1 112 ) (< V1 121)) 

)) ; Limits 1, 0, 8, 128

...... 

(assert ( or (and (> V46 0 ) (< V46 9)) (and (> V46 16 ) (< V46 25)) (and (> V46 32 ) (< V46 41)) (and (> V46 48 ) (< V46 57)) (and (> V46 64 ) (< V46 73)) (and (> V46 80 ) (< V46 89)) (and (> V46 96 ) (< V46 105)) (and (> V46 112 ) (< V46 121)) 

)) ; Limits 46, 0, 8, 128

Finally the "next to" constraint is added for each pair of number that must be next to each other 1&2, 2&3, 3&4 etc up to 44&45. The number (position of) V1 must be +/- 1,15,16,17 different from V2. 

(assert ( or 

(= 1  (- V2 V1)) (= 1  (- V1 V2))  (= 15 (- V2 V1)) (= 15 (- V1 V2)) 

(= 16 (- V2 V1)) (= 16 (- V1 V2))  (= 17 (- V2 V1)) (= 17 (- V1 V2)) )) ; next2M 2 1

(assert ( or 

(= 1 (- V2 V3)) (= 1 (- V3 V2)) (= 15 (- V2 V3)) (= 15 (- V3 V2)) 

(= 16 (- V2 V3)) (= 16 (- V3 V2)) (= 17 (- V2 V3)) (= 17 (- V3 V2))

)) ; next2P 2 3

......

(assert ( or (= 1 (- V45 V44)) (= 1 (- V44 V45)) (= 15 (- V45 V44)) (= 15 (- V44 V45)) (= 16 (- V45 V44)) (= 16 (- V44 V45)) (= 17 (- V45 V44)) (= 17 (- V44 V45)) )) ; next2M 45 44

and finally submit the model which is 223 lines for this puzzle.

(check-sat)

(get-value (V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 ))

(exit)

The perl script ./hidato_smt2.pl is passed the puzzle file hi_002.txt and generates the SMT2 logic lines that are saved into file  hi_002.smt2 and passed to the solver_m5. The output of which is again passed through the script to generate the display output in file hi_002.html All achieved with this single unix command line.

$ ./hidato_smt2.pl < hi_002.txt | tee hi_002.smt2 | ../solver_m5 | tee hi_002.m5 | ./hidato_smt2.pl -f hi_002.txt > hi_002.html 

The results are checked in the script to ensure that the numbers are sequentially positioned. The placed numbers are sequentially coloured by the script. The solver takes about 1.3s on an i7 MacBook Pro for this puzzle and 2.15 for the larger puzzle.

		13	11	10	7
	15	14	12	8	9	6
18	16			24	1	3	5
17	19		25	23	2	44	4
30	31	20	22	26		45	43
32	29	21	27			42	46
	33	28	35	36	40	41
		34	37	38	39

Numbers: 1 .. 46 
1 OK, 2 OK, 3 OK, 4 OK, 5 OK, 6 OK, 7 OK, 8 OK, 9 OK, 10 OK, 11 OK, 12 OK, 13 OK, 14 OK, 15 OK, 16 OK, 17 OK, 18 OK, 19 OK, 20 OK, 21 OK, 22 OK, 23 OK, 24 OK, 25 OK, 26 OK, 27 OK, 28 OK, 29 OK, 30 OK, 31 OK, 32 OK, 33 OK, 34 OK, 35 OK, 36 OK, 37 OK, 38 OK, 39 OK, 40 OK, 41 OK, 42 OK, 43 OK, 44 OK, 45 OK, 46 OK, 

A larger Hidato puzzle

		5	6	7	11	13	14	15	18
			4	8	10	12	16	17	19
76				3	9	35	33	20	21
75	77			2	36	34	32	30	22
74	72	78	79	1	37	38	31	29	23
73	46	71	43	42	41	40	39	28	24
47	45	44	70	69	55			27	25
48	50	52	68	54	56				26
49	51	67	53	57	62	59
	66	65	64	63	58	61	60

Number : 1 .. 79 
1 OK, 2 OK, 3 OK, 4 OK, 5 OK, 6 OK, 7 OK, 8 OK, 9 OK, 10 OK, 11 OK, 12 OK, 13 OK, 14 OK, 15 OK, 16 OK, 17 OK, 18 OK, 19 OK, 20 OK, 21 OK, 22 OK, 23 OK, 24 OK, 25 OK, 26 OK, 27 OK, 28 OK, 29 OK, 30 OK, 31 OK, 32 OK, 33 OK, 34 OK, 35 OK, 36 OK, 37 OK, 38 OK, 39 OK, 40 OK, 41 OK, 42 OK, 43 OK, 44 OK, 45 OK, 46 OK, 47 OK, 48 OK, 49 OK, 50 OK, 51 OK, 52 OK, 53 OK, 54 OK, 55 OK, 56 OK, 57 OK, 58 OK, 59 OK, 60 OK, 61 OK, 62 OK, 63 OK, 64 OK, 65 OK, 66 OK, 67 OK, 68 OK, 69 OK, 70 OK, 71 OK, 72 OK, 73 OK, 74 OK, 75 OK, 76 OK, 77 OK, 78 OK, 79 OK

Broken puzzle detection

Finally we check that impossible puzzle configurations are detected. Taking the above hi_002.txt file we change the positions of the 10 & 23 clue.

$ diff hi_002.txt hi_002XBroken.txt

2c2

< x,x,0,0,10,0

---

> x,x,0,0,23,0

5c5

< 17,0,x,0,23,0,0,4

---

> 17,0,x,0,10,0,0,4

The solver reports that the problem is "unsat" unsatisfiable.

$ ./hidato_smt2.pl < hi_002XBroken.txt | ../solver_m5 

unsat

(error "model generation not enabled")

Some Curios

The very insightful researcher Denis Berthier at Ecole Polytechnic explore in depth the logic behind a puzzle specific solving methods for various puzzles. In the section on Hidato these gems are listed.

Each of which solves quickly using the Mathsat5 solver ( after the end square number is added).

Me_BA.txt

../../solver_mathsat5  2.38s user 0.03s system 98% cpu 2.453 total

./hidato_smt.pl -f $i > $i.html  0.01s user 0.01s system 0% cpu 2.452 total

Me_BB.txt

../../solver_mathsat5  1.60s user 0.01s system 99% cpu 1.613 total

./hidato_smt.pl -f $i > $i.html  0.00s user 0.00s system 0% cpu 1.614 total

Me_BC.txt

../../solver_mathsat5  0.16s user 0.00s system 97% cpu 0.166 total

./hidato_smt.pl -f $i > $i.html  0.00s user 0.00s system 4% cpu 0.166 total

Knights Tour

The knights tour puzzle is very similar to the Hidato except that the step to next square in sequence is made using a chess knights move of one step orthogonally and one diagonally away from the starting space. Knights can jump over squares as part of the move but in the same way as Hidato must cover every open square in the puzzle in the order specified by the clues. A knights move will always change square colour on a regular chess board.  

The solver file preparation software was change to include :

A -k option to switch to knights move logic, different move constrain logic and solution checking software. The input and display logic remains unchanged. 

From this input file 

#ktour ktour_003.txt 10x10

45,0,0,52,43,18,0,74,0,0

48,0,0,0,94,0,0,19,84,0

0,0,53,0,57,0,0,0,0,40

0,0,0,91,98,0,72,0,76,0

59,14,0,0,81,90,0,0,0,0

2,0,64,0,100,0,82,0,86,0

0,0,1,0,0,68,87,78,23,38

0,0,66,63,0,35,70,0,0,29

0,12,0,0,69,0,33,0,0,0

4,7,0,11,0,0,0,25,0,31

Comparing the logic generated for the Hidato “next step” logic with that for the knights tour the difference in values I can be seen

Hidato :

(assert ( or (= 1 (- V2 V3)) (= 1 (- V3 V2)) (= 19 (- V2 V3)) (= 19 (- V3 V2)) (= 20 (- V2 V3)) (= 20 (- V3 V2)) (= 21 (- V2 V3)) (= 21 (- V3 V2)) )) ; next2P 2 3

Knights Tour :

(assert ( or (= 18 (- V2 V3)) (= 18 (- V3 V2)) (= 22 (- V2 V3)) (= 22 (- V3 V2)) (= 41 (- V2 V3)) (= 41 (- V3 V2)) (= 39 (- V2 V3)) (= 39 (- V3 V2)) )) ; next2P 2 3

The solver finds this knights tour route

The solver does bog down if insufficient clue squares are provided.

References

Programming Z3 Sudoku section from Section 8.1 page 139

Pattern-Based Constraint Satisfaction and Logic Puzzles - Denis Berthier

Building a Sudoku Solver with SAT,  

A SAT-based Sudoku Solver,  

Sudoku as a SAT Problem, 

Optimized CNF Encoding for Sudoku Puzzles 

Mathsat5 solver

Usage for the Hidato to SMT generation utility

Usage: hidato/kTour {options} < puzzle.txt  or

    hidato {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

    -k use knight chess moves rather than kings piece ( Hidato ) moves.

        

    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

        Using unique numbers complete the partly filled grid.

        The numbers should count from lowest to highest moving up,down,left,right or diagonally.

Each hidato puzzle Input as follows (needs to be filled out to a rectangular grid) else blocking square constraints not completed corectly ( bug )

        

        #Hidato dm unk hi_002.txt

        x,x,0,0,10,0

        x,0,14,12,0,9,0

        0,16,x,x,0,1,0,0

        17,0,x,0,23,0,0,4

        30,0,0,0,26,x,45,0

        0,0,0,0,x,x,0,46

        x,0,28,0,0,40,0

        x,x,0,37,38,39

    

    Knights Tour type puzzle has the start and finish number and some intermediate steps. Uses the -k flag to set this mode

#ktour ktour_003.txt 10x10

45,0,0,52,43,18,0,74,0,0

48,0,0,0,94,0,0,19,84,0

0,0,53,0,57,0,0,0,0,40

0,0,0,91,98,0,72,0,76,0

59,14,0,0,81,90,0,0,0,0

2,0,64,0,100,0,82,0,86,0

0,0,1,0,0,68,87,78,23,38

0,0,66,63,0,35,70,0,0,29

0,12,0,0,69,0,33,0,0,0

4,7,0,11,0,0,0,25,0,31

    

    

        The internal working %matrix has -1 for Blocks 'x' and -2 for edge fills on RHS

....

to generate an SMT2 input file.

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

            

Puzzle checks will fail with these messages

**ERROR Numbers of holes => there are not enough 0 holes to put the missing numbers between 1..last

**ERROR Duplicate Clue Number => rerun with -v 4 and look on the "Values: Should all be =1"  line for ERROR

Other sets of Hidato puzzles

Including a couple of broken ones that need investigation.

Updated 08 Dec 2025