Solving Kakuro using an SMT (Integer) solver ** updated 2026 **

** Update 2026 - A couple of larger puzzles of this type have been included below **

Continuing in the short series of reframing puzzles and using an SMT integer solver to find a solution we look now at solving the Kakuro class of problem.  This popular number placement puzzle seen in the UK papers Daily Telegraph and Daily Mail. This puzzle is similar to Sudoku using a rectangular grid of numbers but differs in that target sums are set for horizontal and vertical lines. The numbers 1..9 are placed in the grid such that the sum of the numbers equals the target provided. Any number can only used once in each horizontal and vertical sum.

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.

A larger example 

Found some larger examples of Kakuro puzzles over at Paul A Grosse pages.

There was a minor issue discovered when encoding these larger examples in that there are single block squares that are not entirely obvious from the puzzle presentation. When two or more block squares are adjacent the border line between them is removed. A single block square can only be identified by the subtle shading or by logic. These have been marked with a red star on the image below.

The solution took 0.29 seconds on a 2012 Core i7 MacBook. 346 lines solved

The source text encoding for the above puzzle is :

#Kakurok k_20061006.txt Paul_A_Grosse

x,x,10\,4\,x,x,x,x,x,16\,9\,x,x,x,x,3\,12\,x,x,x,x,x,4\,20\,x

x,17\4,0,0,3\,x,x,x,22\17,0,0,x,x,x,\10,0,0,23\,x,x,x,9\6,0,0,3\

\14,0,0,0,0,21\,x,17\13,0,0,0,x,x,x,\6,0,0,0,10\,x,30\10,0,0,0,0

\13,0,0,17\3,0,0,14\9,0,0,x,x,x,x,x,x,x,\4,0,0,17\17,0,0,16\4,0,0

x,\9,0,0,29\30,0,0,0,0,17\,x,x,x,x,x,x,17\30,0,0,0,0,29\17,0,0,x

x,x,\29,0,0,0,0,6\12,0,0,17\,24\,x,x,23\,9\16,0,0,17\30,0,0,0,0,x,x

x,x,x,16\16,0,0,15\28,0,0,0,0,0,x,\34,0,0,0,0,0,34\13,0,0,17\,x,x

x,x,7\17,0,0,4\10,0,0,0,\17,0,0,6\,16\8,0,0,\13,0,0,0,6\16,0,0,6\,x

x,11\22,0,0,0,0,0,0,x,x,\29,0,0,0,0,x,x,\38,0,0,0,0,0,0,11\

\4,0,0,x,\3,0,0,11\,x,x,x,\10,0,0,x,x,x,x,11\10,0,0,x,\4,0,0

\10,0,0,23\,4\,\7,0,0,x,x,x,x,x,x,x,x,x,\6,0,0,x,17\,39\10,0,0

x,x,\4,0,0,\4,0,0,11\,x,x,x,x,x,x,x,21\,3\11,0,0,\17,0,0,x,x

x,x,16\3,0,0,16\,9\13,0,0,x,x,x,x,x,x,\7,0,0,0,3\,16\16,0,0,3\,x

x,\14,0,0,9\13,0,0,0,0,16\,x,x,x,x,x,16\24,0,0,0,0,0,16\6,0,0,x

x,\34,0,0,0,0,0,\9,0,0,11\,x,x,x,11\15,0,0,x,\25,0,0,0,0,0,x

x,x,30\4,0,0,x,x,x,\17,0,0,3\,x,6\17,0,0,x,x,x,x,\13,0,0,30\,x

x,17\17,0,0,x,x,x,x,x,\4,0,0,6\4,0,0,x,x,x,x,x,x,\17,0,0,16\

\15,0,0,x,x,x,x,x,x,x,\6,0,0,0,8\,x,x,x,x,x,x,x,\17,0,0

\17,0,0,22\,x,x,x,x,x,x,x,4\6,0,0,0,17\,x,x,x,x,x,x,38\13,0,0

x,\10,0,0,3\,x,x,x,x,x,17\3,0,0,\16,0,0,4\,x,x,x,x,17\16,0,0,x

x,x,4\8,0,0,16\,11\,x,x,11\11,0,0,x,x,\11,0,0,6\,x,16\,7\17,0,0,6\,x

x,\18,0,0,0,0,0,30\,9\16,0,0,x,x,x,x,\3,0,0,10\34,0,0,0,0,0,x

x,\6,0,0,3\34,0,0,0,0,0,x,x,x,x,x,x,\13,0,0,0,0,4\5,0,0,x

x,x,\3,0,0,x,15\7,0,0,x,x,x,x,x,x,x,\5,0,0,15\,\6,0,0,x,x

x,11\,7\5,0,0,\14,0,0,x,x,x,x,x,x,x,x,x,\3,0,0,\9,0,0,24\,10\

\10,0,0,x,x,14\12,0,0,x,x,x,x,17\,3\,x,x,x,\4,0,0,3\,x,\17,0,0

\4,0,0,16\,11\11,0,0,7\,x,x,x,9\9,0,0,23\,x,x,x,16\4,0,0,30\,17\8,0,0

x,\22,0,0,0,0,0,0,39\,x,11\25,0,0,0,0,6\,x,38\37,0,0,0,0,0,0,x

x,x,\10,0,0,11\11,0,0,0,3\4,0,0,x,\7,0,0,17\15,0,0,0,11\17,0,0,x,x

x,x,x,3\4,0,0,5\20,0,0,0,0,0,x,\35,0,0,0,0,0,3\11,0,0,4\,x,x

x,x,11\11,0,0,0,0,3\8,0,0,x,x,x,x,x,\16,0,0,13\15,0,0,0,0,10\,x

x,3\3,0,0,13\17,0,0,0,0,x,x,x,x,x,x,x,\11,0,0,0,0,3\4,0,0,3\

\3,0,0,3\12,0,0,\6,0,0,16\,17\,x,x,x,x,3\,4\17,0,0,\3,0,0,4\4,0,0

\10,0,0,0,0,x,x,\24,0,0,0,x,x,x,\8,0,0,0,x,x,\10,0,0,0,0

x,\7,0,0,x,x,x,x,\16,0,0,x,x,x,\4,0,0,x,x,x,x,\3,0,0,x

The next one to try ....

The solution took 0.28 seconds on a 2012 Core i7 MacBook. 280 lines solved.

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

Script

The script that both processes the text representation generating SMT-2 constraint lines and reads the results of the solver and creates the result display has the follow in Usage ..

Usage : Kakuro_solver {options} puzzle.txt

  -v x set debug level 0..10

  -h Generate usage message

  -f puzzleFile.txt from which .html will be generated (used when reading solver output only)

  -p  .html will be generated from puzzleFile.txt on STDIN (does not generate solver output)

    Programs reads STDIN looking for either puzzleFile format lines or Solver output lines

    If the input is in puzzleFile.txt program will generate solver input lines unless -p is given in which case .html version of the board is generated.

    If the input is solver output lines the program will expect a -f puzzleFile.txt parameter. From both these input streams program will then generate display .html output.

    

Input puzzleFile format is rectangular with each square being any of target number down/target number across, 0=target square, #=comment line, x=block square

Note: Last line of puzzle must be padded out to full width with tailing ,x blocks if necessar 

    

Example puzzleFile :

#k_003.txt No 322 Diabolic

x,x,45/,20/,x,x,12/,4/,45/,x

x,24/13,0,0,x,13/7,0,0,0,23/

/13,0,0,0,26/30,0,0,0,0,0

/33,0,0,0,0,0,13/,14/9,0,0

/17,0,0,4/35,0,0,0,0,0,0

.... and so on but use the other /

Example Solver output format

sat

    ( (V12 8)

    (V13 6)

    (V16 3)

    (V17 1)

....

    

    May issue a

    **ERROR** Missing ... if invalid input equation is detected ie  ,x12/ or

    **ERROR** Single Digit target sum ... if invalid single digit target sum is found