Solving Sujiko using an SMT (integer) solver

This blog entry describes how the Sujiko puzzle is deconstructed into logic lines suitable for a solver such as Z3 or MathSat.

Sujiko is a simple arithmetic puzzle where fours simultaneous sums have to be satisfied. Each of the eight empty squares have to be filled with non-repeating numbers 1 to 9 such that the target numbers in the circles are the sum of the surrounding numbers. A clue number is provided.

Sample Sujiko from The Daily Telegraph

Encoding 

The input puzzle can be represented as a text file su_001.txt in this format : 

#sujiko DT_3072

25,13,22,17

P8,6

The first line being a comment, the second the target numbers and finally the clue number as Position 8 value 6.

Puzzle Logic

In this puzzle each of the answer squares are numbered V0 to V8 with the targets numbered T0 to T3.  In the solution T0 must equal V0 + V1 + V3 + V4  and T1=V1 + V2 + V4 +V5 ( similarly for T2 & T3).  Each of the V.. numbers must be between 1 and 9 inclusive but all different.

In essence this is a four simultaneous equation problem with 8 unknowns. There are 362,880 possible Sujiko puzzles being the number of ways that 1..9 can be arranged ( permutations ).

Variables and Targets

Building the SMT-Lib file

Converting the input target and clue into logic lines for the solver is the next stage. Using the SMT-Lib language to describe the problem is the bridge between problem and solver ready solution. The logic lines start with a preamble describing the type of logic being used then each of the unknowns are declared, limited to a range and linked to the other numbers with relationships. 

In the pre-amble we set the solver into integer mode and declare that answer and values will be need beyond proof that the puzzle can be solved.

(set-logic LIA)

(set-option :produce-models true)
(set-option :produce-assignments true)

Each of the targets are declared and set to the required value ...

(declare-const T0 Int)

(assert (= T0 25 ))

(declare-const T1 Int)

(assert (= T1 13 ))

(declare-const T2 Int)

(assert (= T2 22 ))

(declare-const T3 Int)

(assert (= T3 17 ))

Each of the answer squares are declared and a range limit is set as bigger than 0 less than 10 ....

(declare-const V0 Int)

(assert (and (> V0 0) (< V0 10)))

(declare-const V1 Int)

(assert (and (> V1 0) (< V1 10)))

(declare-const V2 Int)

(assert (and (> V2 0) (< V2 10)))

....

(declare-const V7 Int)

(assert (and (> V7 0) (< V7 10)))

(declare-const V8 Int)

(assert (and (> V8 0) (< V8 10)))

The answers must be uniquely different values .....

(assert (distinct V0 V1 V2 V3 V4 V5 V6 V7 V8  ))

The clue is provided by setting V8 to 6

(assert (= V8 6)); Clue provided

finally the sums are configured and the run commands provided....

(assert (= T1 (+ V1 V2 V4 V5)))

(assert (= T2 (+ V3 V4 V6 V7)))

(assert (= T3 (+ V4 V5 V7 V8)))

(assert (= T0 (+ V0 V1 V3 V4)))

(check-sat)

(get-model)

(exit)

Running the solver and displaying the output

The input text puzzle is generated into logic lines using a script. The script output is passed to the solver that will in turn generate "sat" and the values of the cells or if the problem cannot be solved "unsat" is returned. The output of the solver is read into the same script and an .html file of results and check lines are presented.  

This is a very small scale problem for the solver that takes about 0.04 seconds to solve on a Mac Book Pro 2011.

The command line used is :

./sujiko_smt.pl < su_001.txt | tee su_001.smt | ../solver_m5 |tee su_001M5.res | ./sujiko_smt.pl -f su_001.txt > su_001.html

The input SMT logic lines above are saved into file  su_001.smt.

The intermediate  results from the solver are collected into file su_001M5.res showing as :

 

sat

(model

  (define-fun T0 () Int 25)

  (define-fun T1 () Int 13)

  (define-fun T2 () Int 22)

  (define-fun T3 () Int 17)

  (define-fun V0 () Int 9)

  (define-fun V1 () Int 3)

  (define-fun V2 () Int 1)

  (define-fun V3 () Int 8)

  (define-fun V4 () Int 5)

  (define-fun V5 () Int 4)

  (define-fun V6 () Int 7)

  (define-fun V7 () Int 2)

  (define-fun V8 () Int 6)

)

Finally the encoding display script generates a web display page into file su_001.html

Error checking 

When the result value V6 is changed to 5 (from 7) the Sequence checks indicate a **Fail** 

References

MathSAT the m5 solver used here.

Z3 the Z3 solver made by Microsoft - get it here

Sujiko

Using SMT for sudoku puzzles

Programming Z3 Sudoku section from Section 8.1 page 139 uses python and a library to build logic lines.

Appendix usage for logic preparation script

Usage: sujiko {options} < puzzle.txt  or

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

  Complete a grid using each of the numbers 1..9 in the positions 0..8 on the game board such that the sums amounts provided as A,B,C,D are the total of these surrounding position squares. E.G. A=Pos0+Pos1+Pos3+Pos4 and D=Pos4+Pos5+Pos7+Pos8

        

        Layout of board for clue positions:

        0 1 2

         A B

        3 4 5

         C D

        6 7 8

        

        P8,6 would mean that position 8 has clue number set to 6.

        

Each sujiko puzzle Input as follows

        

    #sujiko DT_3072

    25,13,22,16

    P8,6

        

OR Process results from solver in the following format

            sat

            (model

              (define-fun T0 () Int 25)

              (define-fun T1 () Int 13)

              (define-fun T2 () Int 22)

    ....

to generate an html page as output.

            

Puzzle checks will fail with these messages

**ERROR Numbers of input Values not = 4