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
Possible Rotors are :
+ = singleOn, one segment is black- = singleOff, one segment is white, three segments are blacko = opposite2, like the BMW logoa = adjacent2, like a 1/2 eaten pie
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)
(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) ))
.....
;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)))
(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 |
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.
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.
