Looking at the incorrectly completed Kakuro diagram below the blue numbers are the answer cells which would be all blank at the start of the puzzle. The green cells are the target sums annotated as "down \ across". The red cells are targets that are not correctly answered. For example on the top row 4\ represents the vertical target sum for the two cells below. As 1+2 = 3 this is not the answer of 4 that we are after. Also the horizontal part of the target sum 15\14 adds up to 13. The other constraint is that any of the digits 0 to 9 can appear only once in a sum. To make total 4 the digits 1 and 3 must be used.
 |
| Incorrectly completed Kakuro |
This puzzle can be prepared for an integer solver by transforming the input puzzle and generating the required propositional SMT-LIB input lines. Starting with the text format of the puzzle as follows:
#Kakuro k_057.txt DM Sat 11May19
x,x,32\,15\,x,x,16\,4\,13\,x
x,18\14,0,0,14\,\10,0,0,0,3\
\28,0,0,0,0,15\14,0,0,0,0
\16,0,0,21\17,0,0,0,16\3,0,0
\14,0,0,0,20\23,0,0,0,24\,12\
\13,0,0,0,0,3\11,0,0,0,0
x,14\,11\13,0,0,0,4\17,0,0,0
\7,0,0,17\7,0,0,0,13\12,0,0
\21,0,0,0,0,\10,0,0,0,0
x,\24,0,0,0,x,\11,0,0,x
Each cell is identified as either a block "X", answer cell "0" or target cell with one or two target sums. For each of the answer cells we declare an int and set a range.
(declare-const V12 Int)
(declare-const V13 Int)
(declare-const V16 Int)
...
(assert (and (> V12 0) (< V12 10)))
(assert (and (> V13 0) (< V13 10)))
(assert (and (> V16 0) (< V16 10)))
...
The slightly tricky bit is generating the target sums and setting the parts of that sum to have unique cell answers. This is achieved by generating a list of the cells involved with each target sum. For Example in cell 11 we have 18\14 that splits into target sums "H11" & "V11". H11 is the sum of cells 12,13 which must be 14 and V11 is the sum of cells 21,31,41,51 which must be 18.
# H11,12,13 is 14
# H15,16,17,18 is 10
# H20,21,22,23,24 is 28
.....
# V11,21,31,41,51 is 18
# V14,24,34 is 14
# V19,29,39 is 3
These are reformatted into the propositional logic lines.... two lines for each equation to see the sum and insist on the uniqueness of the involved cells.
(assert (= 14 (+ V12 V13 )))
(assert (distinct V12 V13 ))
(assert (= 10 (+ V16 V17 V18 )))
(assert (distinct V16 V17 V18 ))
(assert (= 28 (+ V21 V22 V23 V24 )))
...
(assert (= 18 (+ V21 V31 V41 V51 )))
(assert (distinct V21 V31 V41 V51 ))
Along with some supporting lines this is all fed into the solver that generates an answer for each cell. The solver for this puzzle takes 0.08s on a MacBook Pro 2.2Hz.
$ ../solver_m5 < k_057.txt.sml
sat
( (V12 8)
(V13 6)
(V16 3)
(V17 1)
(V18 6)
(V21 8)
(V22 6)
.....
A script is used to generate the solver lines from the puzzle and re-used to read the answers from the solver to generate the html format for the output picture. The script also checks the answers and colours the target sum cells red if a failure is detected. The correct answer, as provided by the solver, is shown here.
$ ./kakuro_SMT2.pl < samples/k_057.txt | ../solver_m5 | ./kakuro_SMT2.pl -f samples/k_057.txt > k_057.html
We could have helped the solver by narrowing the range of each answer cell. For example to make the target sum 17 with two numbers only 8 and 9 are candidates for the answer cells. Adjusting the lines
(assert (and (> V87 0) (< V87 10)))
(assert (and (> V97 0) (< V97 10)))
to
(assert (and (> V87 7) (< V87 10)))
(assert (and (> V97 7) (< V97 10)))
would have narrowed the work needed by the solver but given the puzzle runtime of under 0.09s this was not considered necessary.
Kakuro table
This table shows the number of choices available for filling target lines of a given length with a given sum. For Example there are 42 ways to make Target 18 using 3 sequence digits.
$ Use_tables.pl -i 3,18
Entry [3,18] = 189 198 279 297 369 378 387 396 459 468 486 495 549 567 576 594 639 648 657 675 684 693 729 738 756 765 783 792 819 837 846 864 873 891 918 927 936 945 954 963 972 981
 |
| Kakuro count table |
No comments:
Post a Comment