Solving Seki using an SMT (integer) solver

This entry describes how the Seki puzzle is deconstructed into logic lines suitable for a solver such as Z3 or MathSat. Other puzzles are available. This article is one of a series reframing logic puzzles into a format suitable for an SMT Integer solver.

Seki is a city in the Gifu province of Japan and the name of a simple logical puzzle. The puzzle has a four by four grid of black or white squares painted according to rotors positioned at the intersection of each four cell group. The task is to set the position of the independent rotors so that each cell is either set black or white.

Encoding

This fixed size puzzle can be encoded using a list of the rotor types showing at the cell intersections. 

Possible Rotors are : 

+ = singleOn, one segment is black

- = singleOff, one segment is white, three segments are black

o = opposite2, like the BMW logo 

a = adjacent2, like a 1/2 eaten pie 

For the puzzle above we have :

oo+ooaoo-

The output of the solution would be the settings of the cells numbered V0 to V15 each with a 1 (black) or 0 (white) assignment.

Cell numbers grid

Puzzle Logic

Whilst the intersection rotors are independently set they have interdependencies with neighbouring rotors. Each rotor must be positioned without conflicts over the cells shared between the rotors. We can see that the rotor types dictates the number of surrounding cells that are set to black. For o and a rotors two cells are set. One and three cells are set for the + and - rotor types. By having 16 cells each set to 1 or 0 we can use the rotors as constraints for the setting of the group of cell values that surround each rotor. The similarity of the o and a rotors require some extra logic to constrain which two of the surrounding cells are set.

Each rotor +, - and "a" rotors have 4 possible positions but the "o" rotor only 2. Depending on the number of o rotors in a given puzzle the maximum number of possible rotor arrangements is  4^9 = 262,144. This particular puzzle has 4^3 + 6^2 = 100 possible arrangements.

Building the SMT-Lib file

With the puzzle rotors encoded, the next stage is to convert the puzzle rotor types into logic lines for a solver. The bridge between problem and solver ready input is the SMT-Lib language. The SMT 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 then linked to the other numbers using a constraint relationships.  63 lines of logic are generated in total for this puzzle.

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

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

Each of the target cells are declared and set to the required value range of 0 or 1. In theory we could use a boolean value for each cell but as the constrains are phrased in terms of the number of cells set in a rotor group using integers limited to value 1 or  0 allows for easier addition.

(declare-const V0 Int) 
(assert (or (= V0 0) (= V0 1) )) 
(declare-const V1 Int) 
(assert (or (= V1 0) (= V1 1) )) 
(declare-const V2 Int) 
(assert (or (= V2 0) (= V2 1) ))
.....  

and on up to V15. The constraints between the cells belonging to each rota are set according to the rotor type. For the + and - rotor types there is a single constraint being the total number of the surrounding cell values. The o and a also have the number of cells set as a constraint but also a further constraint line enforcing the rotor pattern type is generated.  o rotors must have one of two pairs of opposite cells set to 1.  a rotors must have one of four pairs of cells set. The combination of constraining the sum of the neighbouring cells and which pairs of cells are set fully described the a rotor constraint.

 

Comment starting with ; are included to annotate the rotorgroup number, rotor type, and cells belonging to that rotor.  



;RotorGroup 0 o 0,1,4,5 
(assert (= 2 (+ V0 V1 V4 V5))) 
(assert (or (= 2 (+ V0 V5)) (= 2 (+ V1 V4)) )); o 
.....
;RotorGroup 2 + 2,3,6,7
(assert (= 1 (+ V2 V3 V6 V7)))
.....
;RotorGroup 5 a 6,7,10,11 
(assert (= 2 (+ V6 V7 V10 V11))) 
(assert (or (= 2 (+ V6 V7)) (= 2 (+ V7 V11)) (= 2 (+ V11 V10)) (= 2 (+ V6 V10)))); a 
.....
;RotorGroup 8 - 10,11,14,15 
(assert (= 3 (+ V10 V11 V14 V15)))

and finally the post-amble to generate the results

(check-sat)

(get-value ( V0 V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15))

(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 (piped) into the same script and an .html file of results and checked lines are presented.  
This is a very small scale problem for the solver that takes about 0.01 seconds to solve on a Mac Book Pro 2011.
The command line used is :

$ ./seki_smt.pl < sk_6018.txt | time ../solver_m5  | ./seki_smt.pl -f sk_6018.txt > sk_6018.html 

   

     0.02 real         0.00 user         0.00 sys

The html file results are seen as follows:

#seki MOS 01Feb2021 sk_6018.txt

1	0	1	0
0	1	0	0
1	0	1	1
0	1	0	1

Check Results

RotorGroup 0 ch=o Value=2 [0,1,4,5] gives Sum = 2 finalRes=0
RotorGroup 1 ch=o Value=2 [1,2,5,6] gives Sum = 2 finalRes=0
RotorGroup 2 ch=+ Value=1 [2,3,6,7] gives Sum = 1 finalRes=0
RotorGroup 3 ch=o Value=2 [4,5,8,9] gives Sum = 2 finalRes=0
RotorGroup 4 ch=o Value=2 [5,6,9,10] gives Sum = 2 finalRes=0
RotorGroup 5 ch=a Value=2 [6,7,10,11] gives Sum = 2 finalRes=0
RotorGroup 6 ch=o Value=2 [8,9,12,13] gives Sum = 2 finalRes=0
RotorGroup 7 ch=o Value=2 [9,10,13,14] gives Sum = 2 finalRes=0
RotorGroup 8 ch=- Value=3 [10,11,14,15] gives Sum = 3 finalRes=0

Puzzle OK Solution successful.

 This problem could be easily scaled up to a much larger size. The usual fail confirmation test is successfully run generating this message if the cell values do not match the rotor type values. 

Puzzle has ** ERROR ** Solution failed by difference = 2.

References

Programming Z3 Sudoku section from Section 8.1 page 139

Building a Sudoku Solver with SAT,  

A SAT-based Sudoku Solver,  

Sudoku as a SAT Problem, 

Optimized CNF Encoding for Sudoku Puzzles 

Appendix usage for logic preparation script

Usage: Seki {options} < puzzle.txt  or

    Seki {options} -f puzzle.txt < SolverOutput

    -v N :Be verbose to level N ( use v=10 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 puzzle File paremeter.

            Using both these input streams program will then generate display .html output.

Game Rules

Given a 4*4 grid with a coloured rotor on each line intersection, colour the grid based on the segments in the rotors ( which can be rotated )

Encode seki - Look at the 9 rotors and encode for type

    Possible Rotors are :

    +  = singleOn only one segment is dark

    -  = singleOff only one segment is light

    o = opposite2 Like the BMW logo

    a = adjacent2 Like a 1/2 eaten pie

    

    $ cat sk_6018.txt

    oo+ooaoo-

OR Process results from solver in the following format

    sat

    ( (V0 9)

    (V1 7)

    (V2 5)

    (V3 3)

    ....

to generate an html layout as output.

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

Solving Kurosu using and SMT (Integer) solver

Solving Kurosu using an SMT (integer) solver

See Original and updates on https://gannett-hscp.blogspot.com  

** UPDATED  May 2023 fix method to Int

Back in 2018 the Kurosu problem was reviewed and solved using a simple two way pattern matching script as noted in the blog here.  This entry looks again at this bit setting puzzle with a view to using an SMT (integer) solver.

Kurosu is essentially a bit setting problem with each cell on a six by six grid having value 0 or X. Each row and column must have three each of 0 and X with no more than two 0 or X (treated as 1) adjacent. No row or column with "111" or "000" is allowed.

Encoding

The puzzle is encoded using 1 for the Xs and 0 making this a binary bit setting problem. The limitation of no 111 and no 000 on a row or column considerably reduces the complexity of the problem. The puzzle above encodes as :

#Kurosu6 DM 01 June 2018

...0.1

0...0.

1.1.1.

..0...

.1.0.1

0....0

Puzzle logic

As seen in the previous analysis there are only 14 line patterns that follow the three sequential bit limitation making 11,222 the total number of puzzle line patterns. However this review is to reset the puzzle for solving using an SMT (Integer) solver. 

Previously the solution was reached by only testing with combinations of the allowable lines but that approach is an unnecessary skip towards the answer. The intent of using an SMT solver is to provide the minimal logic and constraints of the puzzle and let the solver figure out the details.

Lines that have three 1 (or 0 ) clue values can be directly solved by setting the gaps to 0 and vice versa but again this is left to the solver to figure out. 

The general approach will be to set up a variable for each cell and describe the relationship between the cells to match the rules of the puzzle. Each cell variable will only be allowed 1 or 0 as values.

Whilst it would seem logical to use a bit based rather than integer solver the syntax and logic available in the QF_BV BitVec version of the SMT solver is tortuous and does not work well for counting bits. Using a constrained value integer allows for the use sum of line value constraints.

 

Row and column cell numbers

The cells of the original puzzle are sequentially numbered and each row and column member cells are established as follows. Each cell is in one row and one column.

For example cell 25 is in column C1 and row R24

#->grpList cell values = 

C0 = 0 6 12 18 24 30!

C1 = 1 7 13 19 25 31!

C2 = 2 8 14 20 26 32!

C3 = 3 9 15 21 27 33!

C4 = 4 10 16 22 28 34!

C5 = 5 11 17 23 29 35!

R0 = 0 1 2 3 4 5!

R12 = 12 13 14 15 16 17!

R18 = 18 19 20 21 22 23!

R24 = 24 25 26 27 28 29!

R30 = 30 31 32 33 34 35!

R6 = 6 7 8 9 10 11!

The constrains of the puzzle are handled in terms of the column and row identifiers. Each row or column line has 6 cell entries. 

Building the SMT-Lib file

In the preamble we set the solver into Linear Integer LIA mode then create 36 single integer V0..V35 to represent each cell and limit the value range. 

(set-logic LIA)

(set-option :produce-models true)

(set-option :produce-assignments true)

(declare-const V0 Int)       ; Declare V0 as an Integer

(assert (or (= V0 0) (= V0 1))) ; This constraint limits the value of V0 to be either 0 or 1

(declare-const V1 Int)

(assert (or (= V1 0) (= V1 1)))

(declare-const V10 Int)

(assert (or (= V10 0) (= V10 1)))

(declare-const V11 Int)

(assert (or (= V11 0) (= V11 1)))

The known clue cells are set ....

(assert (= V3 0 ))

(assert (= V5 1 ))

(assert (= V6 0 ))

(assert (= V10 0 ))

(assert (= V12 1 ))

…

(assert (= V35 0 ))

In overview each cell belongs to one row and one column. Each row and column has 6 cell; the overall row and column values are constrained to add up to 3. Each of the row and columns are built into 5 constrains. The first being that the sum of values must be 3 and then for each set of three cells the sum must be 2 or less. The less than 3 constraint on each group of 3 cells across each line ensures that the “no adjacent sets of 3 1 values” game rule is enforced. As there are only 6 cells in a row by enforcing the no 3 adjacent 1 cells, rule the no 3 zeros rule is also delivered.

(assert (= 3 (+ V0  V6  V12  V18  V24  V30 ))); Region C0

(assert (> 3 (+ V0 V6 V12 ))); Sub group of C0

(assert (> 3 (+ V6 V12 V18 ))); Sub group of C0

(assert (> 3 (+ V12 V18 V24 ))); Sub group of C0

(assert (> 3 (+ V18 V24 V30 ))); Sub group of C0

…..

(assert (= 3 (+ V0  V1  V2  V3  V4  V5 ))); Region R0

(assert (> 3 (+ V0 V1 V2 ))); Sub group of R0

(assert (> 3 (+ V1 V2 V3 ))); Sub group of R0

(assert (> 3 (+ V2 V3 V4 ))); Sub group of R0

(assert (> 3 (+ V3 V4 V5 ))); Sub group of R0

A set of constraint lines are generated for each of the regions C0 to C5 and R0 to R6 as shown above. The following lines cause the solver evaluate the model and generate then display the resulting values.

(check-sat)

(get-model)

(exit)

151 lines of logic are needed to represent this instance of the puzzle. 

The solver has to choose the values for the cells such that all the constraints are met.

Running the solver and displaying the output

The input puzzles 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, rows and columns or if the problem cannot be solved "unsat" is seen. The output of the solver is processed by the same script and an .html file of results and check lines is presented.  The bold values are the clue numbers.

The mathSAT solver finds the answer in less than 0.08s on a MacBook pro 2011 and in 0.02s on a 2022 Mac mini.

The output of the solver is a list of values for each cell.

                                                                  

sat

(model

  (define-fun V0 () Int 1)

  (define-fun V1 () Int 1)

  (define-fun V10 () Int 0)

  (define-fun V11 () Int 1)

  (define-fun V12 () Int 1)

…..

These lines are processed into an HTML table with checks for correct solution.

Error checking

If a solver line output is adjusted the script would flag incorrect column or row total values only. Here sed is used to intercept the values as they flow from the solver to the display script. V10 is changed to be the illegal value 2.

% i="ku_dm_01062018.txt"

% perl kurosu_smt.pl  < $i | time ../../solver_mathsat5| sed '/V10/s/[01])/2)/'| perl kurosu_smt.pl -f $i > xxxxBusted.html

%  open xxxxBusted.html

Scaling up considerations

This puzzle could possibly appear in larger formats. The same constraint generation logic could be used. 

Appendix usage for logic preparation script

Usage: kurosu_smt {options} < puzzle.txt  or

    kurosu_smt {options} -f puzzle.txt < SolverOutput

    -v N :Be verbose to level N ( use v=10 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

        6 * 6 matrix of 1/0/.

        Each Row/Column must have 3 * 0 and 3 * 1

        Positioning - No more than 2 lots of 0 and 1 allowed as row or Column neighbours.

        puzzle is printed with 0 & X

        

Encode kurosu puzzle Input as follows, . for unknown and clue 1 and 0 included.

     ku_dm_01062018.txt

    #Kurosu6 DM 01 June 2018

    ...0.1

    0...0.

    1.1.1.

    ..0...

    .1.0.1

    0....0

OR Process results from MathSat solver in the following format

    sat

    (model

      (define-fun V0 () Int 0)

      (define-fun V1 () Int 1)

      (define-fun V10 () Int 0)

      (define-fun V11 () Int 0)

    .....

    To generate an html layout as output.

Run as

    ./kurosu_smt.pl < ku_dm_01062018.txt | ../solver_m5 | ./kurosu_smt.pl -f ku_dm_01062018.txt >  ku_dm_01062018.html

    

/*  Valid Line patterns

[0] 11 = 0x0b = 001011

[1] 13 = 0x0d = 010011

[2] 19 = 0x13 = 001101

[3] 21 = 0x15 = 010101

[4] 22 = 0x16 = 100101

[5] 25 = 0x19 = 011001

[6] 26 = 0x1a = 101001

[7] 37 = 0x25 = 010110

[8] 38 = 0x26 = 100110

[9] 41 = 0x29 = 011010

[10] 42 = 0x2a = 101010

[11] 44 = 0x2c = 110010

[12] 50 = 0x32 = 101100

[13] 52 = 0x34 = 110100

*/