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
*/
