Total Concentration from The Turing Tests - Expert Numbers puzzles, solved using SMT (Integer) solver.

Page 10 of the Expert Number Puzzle book gives us a straight forward "Total Concentration" puzzle to solve. This puzzle is also known as "Cross sum" when presented as a 4 by 4 version in some newspapers.

This puzzle consists of a central seven by seven central grid with row and column totals alongside. There are also two clue numbers at each end of the diagonals. The rows and columns must have numbers placed in the blank squares to add up to the row and column totals. The squares along the two diagonals must also add up to the given clue squares.

 The puzzle is encoded into a text format suitable for reading by a script that will generate the logic lines required by the solver.

#tc Total Concentration - Turing Puzzles P10

70

x,16,2,x,21,x,5,114

6,14,17,20,x,1,x,86

23,12,2,x,x,15,30,106

22,8,x,18,17,x,8,112

2,4,x,x,21,25,18,106

5,x,26,3,12,14,x,98

x,22,21,1,17,x,9,104

102,86,102,100,110,109,117,106

After the clues have been read the logic formulas are generated by rows, columns and diagonals. Firstly an integer variable is created for each square of the puzzle, numbered along the rows staring with V0 as the top diagonal value.

Some set up line included then each variable defined as an iteger with a following line to set the squares' value if known.

(set-logic LIA)

(set-option :produce-assignments true)

(set-option :produce-models true)

(declare-const V0 Int)

(assert (= V0 70 ))

(declare-const V1 Int)

(declare-const V2 Int)

(assert (= V2 16 ))

(declare-const V3 Int)

(assert (= V3 2 ))

.... up to V64

followed by 

;Build the formulas rows

(assert (= V8 (+ V1 V2 V3 V4 V5 V6 V7 )))

(assert (= V16 (+ V9 V10 V11 V12 V13 V14 V15 )))

(assert (= V24 (+ V17 V18 V19 V20 V21 V22 V23 )))

(assert (= V32 (+ V25 V26 V27 V28 V29 V30 V31 )))

(assert (= V40 (+ V33 V34 V35 V36 V37 V38 V39 )))

(assert (= V48 (+ V41 V42 V43 V44 V45 V46 V47 )))

(assert (= V56 (+ V49 V50 V51 V52 V53 V54 V55 )))

;Build the formulas Cols

(assert (= V57 (+ V1 V9 V17 V25 V33 V41 V49 )))

(assert (= V58 (+ V2 V10 V18 V26 V34 V42 V50 )))

(assert (= V59 (+ V3 V11 V19 V27 V35 V43 V51 )))

(assert (= V60 (+ V4 V12 V20 V28 V36 V44 V52 )))

(assert (= V61 (+ V5 V13 V21 V29 V37 V45 V53 )))

(assert (= V62 (+ V6 V14 V22 V30 V38 V46 V54 )))

(assert (= V63 (+ V7 V15 V23 V31 V39 V47 V55 )))

;Build the formulas diagonals R-L

(assert (= V64 (+ V1 V10 V19 V28 V37 V46 V55 )))

;Build the formulas diagonals L-R

(assert (= V0 (+ V49 V42 V35 V28 V21 V14 V7 )))

(check-sat)

(get-value (V0 V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 V47 V48 V49 V50 V51 V52 V53 V54 V55 V56 V57 V58 V59 V60 V61 V62 V63 V64 ))

(exit)

These logic lines are presented to the solver which will solve the logic lines and provide a value of each of the unknown variables. 

sat

( (V0 70)

  (V1 28)

  (V2 16)

  (V3 2)

  (V4 18)

  (V5 21)

.... up to 

  (V61 110)

  (V62 109)

  (V63 117)

  (V64 106) )

The generation script is also used to read the solution lines, alongside with the original puzzle, to generate an html view of the solution. The script also checks the row and column totals for correctness. The clue numbers are show in green, the total squares in red and the answers in blue. 

The logic generation script could have generated partial sums for the provided integers clues but the solver run time of less than 0.03s show this as unnecessary. The script generated 141 logic lines. The constraint of values to 1..30 was also not required for this instance but could be included as part of the integer definition.

The Mathsat5  solver was used to complete this puzzle using the SMT language as input.

Script usage

./ttt_p10.pl -h

Usage:

    Total_Concentration {options} < puzzle.txt  or

    Total_Concentration {options} -f puzzle.txt < SolverOutput

    -v N :Be verbose to level N ( use N=10 for very detailed output )

    -f puzzle.txt :Puzzle file needed when reading Solver output use STDIN otherwise

Train Tracks puzzle explored with an SMT (integer) solver

 Looking now at the Train Tracks puzzle as seen in the Daily Mail newspaper. A couple of examples shown here:

The puzzle is set in an eight by eight grid with integers between 1 and 8 on both the top row and right hand side. Entry and exit points marked A and B are shown with a few grid track sections "clues" provided.  The aim of the puzzle is to complete the train tracks between the start and finish edges including the clue pieces with the constraints :

• The number of track pieces in each row and column must add up to the number attached to that row or column,
• The track can have no gaps or crossovers using only the pieces shown here,
• The track can not have any isolated loops. 

Track pieces, numbered using the edge connections, as shown in Bit Sets

Puzzle encoding 

For this puzzle .. 

Becomes the text file ....  

#tt tt_DM_31102025.txt                                                   

R,3,4,3,5,2,7,4,5

3,0,0,0,0,0,0,0,0

2,0,0,0,10,0,0,0,0

4,0,0,0,0,0,0,0,0

5,5,0,0,0,0,0,0,0

1,0,0,0,0,0,0,0,0

5,0,0,0,0,0,0,0,10

7,0,0,0,0,0,0,0,0

6,0,0,6,0,0,0,0,0

Translating the puzzle into SMT logic

This puzzle looks simple but once examined in detail becomes quite complex due to the edge boundaries.

There are four layers of logic that build different constraints for the solution.  Firstly the row and column targets generate limits on the number of tiles allowed in each row and column. Secondly the tiles must be placed in a single trail across the board joining start to finish. Thirdly the correct tiles must be used to connect the entry and exit points and at each step of the trail. Finally the track may not exit the board other than at the pre-determined entry and exit points.

Firstly a variable ( V0 .. V63) is defined one for each of the squares on the board. The numbers trace along each rows, left to right. Each of those variables are limited to the values ( 0,3,5,6,9,12,10 ) being each of the tiles types defined above.

(declare-const V0 Int)

(assert (or (= 0 V0) (= 5 V0) (= 9 V0) (= 12 V0) (= 6 V0) (= 10 V0) (= 3 V0) ))

(declare-const V1 Int)

(assert (or (= 0 V1) (= 5 V1) (= 9 V1) (= 12 V1) (= 6 V1) (= 10 V1) (= 3 V1) ))

(declare-const V2 Int)

(assert (or (= 0 V2) (= 5 V2) (= 9 V2) (= 12 V2) (= 6 V2) (= 10 V2) (= 3 V2) ))

(declare-const V3 Int)

..... up to V63

Next a variable for each of the column and row targets ( RT0 .. RT7 and CT0..CT7) is defined along with it's value as taken from the top row and left hand side of the puzzle definition.

(declare-const RT0 Int)

(assert (= 3 RT0 ))

(declare-const CT0 Int)

(assert (= 3 CT0 ))

(declare-const RT1 Int)

(assert (= 2 RT1 ))

(declare-const CT1 Int)

(assert (= 4 CT1 ))

..... up to RT7 and CT7

At the top of the logic definition file a few service functions are defined. The first one used is the cnz ( count non-zero) function that will return 1 when a cell value is 1 or above, or 0 if the cell value is 0. 

Note that the logic of "if" appears to only work in some versions of the Z3 solver.

; defining my own sum operator to count non-zero squares

  (define-fun cnz ((x Int)) Int

      (if  (> x 0)  1  0 ))

The function is used to constrain the number of tiles in each columns and rows to the total defined as part of the puzzle.

(assert (= RT0 (+ (cnz V0) (cnz V1) (cnz V2) (cnz V3) (cnz V4) (cnz V5) (cnz V6) (cnz V7)  )))

(assert (= CT0 (+ (cnz V0) (cnz V8) (cnz V16) (cnz V24) (cnz V32) (cnz V40) (cnz V48) (cnz V56)  )))

(assert (= RT1 (+ (cnz V8) (cnz V9) (cnz V10) (cnz V11) (cnz V12) (cnz V13) (cnz V14) (cnz V15)  )))

(assert (= CT1 (+ (cnz V1) (cnz V9) (cnz V17) (cnz V25) (cnz V33) (cnz V41) (cnz V49) (cnz V57)  )))

.... up to RT7 and CT7

From here on the logic is about ensuring that only the tiles with matching edges can be set next to each other and that the track remains on the board.

Looking at the board diagram below it can be seen that there are regions of similar squares that can be treated in the same way.  Each tile squares' possible value depends on the value of its neighbouring squares, thus the treatment, in logic, of a square depends on the what neighbour squares it has.  The corners are individual, four lots of groups of eights round the edges and the remaining inner squares. 

For the corners, if not set as a clue square, then any corner can only be unset or the matching corner piece. ie: Tile 3 for corner square 0, tile 9 for corner square 56.

For example corner square 56, if not explicitly set as a clue, can only be 0 (unset) or tile type 9. If square 56 is set to 9 then the neighbours (48 & 57) must have tiles that join the track correctly.  The functions isUp and isRight are used to constrain the neighbouring tiles.

; Make corner 56 ( known [56] = 0 ) Should be 0 or set in known 

( assert (or (= 0 V56) (= 9 V56)))

( assert (or (not (= 9 V56))  (and (= 9 V56) (and ( isUp V48 ) ( isRight V57 ))) ))

Function isUp and isRight are defined as :

; defining my isRight operator to look at number pair compatibility

; Does square y have a tiles that connect in the left direction ?

    (define-fun isRight ((y Int)) Bool

               ( or (= y 5) (= y 6) (= y 12)))

    (define-fun isUp ((y Int)) Bool

                ( or (= y 3) (= y 6) (= y 10)))

The functions isLeft and isDown match this logic but using matching tile types for the function.

For the edge strips, when not set as a clue piece, only the tiles that keep the track on the board are allowed. ie: Tiles 10,3,9 on the left hand edge squares 8,16,24 but different tile sets limits apply on the other groups of edge squares.

For square 8 and similar for the other squares on the left edge. First the square is limited to the applicable tiles (9, 3, 10) then the consequences of a tile being set on the neighbours are checked.  Some of the secondary lines, are moot but add no cost to the solution.

 

; Make Edges from 8 step 8 to 56 V_17

( assert (or (= 0 V8) (= 9 V8 ) (= 3 V8 ) (= 10 V8 ) ))

( assert (or (not (= 5 V8))  (and (= 5 V8)          ( isRight V9 )) ))

( assert (or (not (= 9 V8))  (and (= 9 V8)   (and   ( isUp V0 ) ( isRight V9 ))) ))

( assert (or (not (= 12 V8)) (and (= 12 V8)         ( isUp V0 )) ))

( assert (or (not (= 6 V8))  (and (= 6 V8)       ( isDown V16 )) ))

( assert (or (not (= 10 V8)) (and (= 10 V8) (and ( isUp V0 ) ( isDown V16 ))) ))

( assert (or (not (= 3 V8))  (and (= 3 V8)  (and ( isRight V9 ) ( isDown V16 ))) ))

For the inner squares, any tile can be placed that conforms to the track continuation (neighbours) and row and column total constraints.

; constr_NextbyEnds next4Me 9 with 10, 8, 17, 1 

( assert (or (not (= 5 V9))  (and (= 5 V9)   (and ( isLeft V8 ) ( isRight V10 ))) ))

( assert (or (not (= 9 V9))  (and (= 9 V9)   (and ( isUp V1 ) ( isRight V10 ))) ))

( assert (or (not (= 12 V9)) (and (= 12 V9)  (and ( isLeft V8 ) ( isUp V1 ))) ))

( assert (or (not (= 6 V9))  (and (= 6 V9)  (and ( isLeft V8 ) ( isDown V17 ))) ))

( assert (or (not (= 10 V9)) (and (= 10 V9) (and ( isUp V1 ) ( isDown V17 ))) ))

( assert (or (not (= 3 V9))  (and (= 3 V9)  (and ( isRight V10 ) ( isDown V17 ))) ))

Using the different combinations of "This square is limited to these tiles" and "when a tile of this type is here the neighbours must have these other types" functions, the main portion of the constraints are built.

The constraints are built by a scripts, the same for every board, with just the the clue tiles and row/column totals varying between instances of the puzzles.

The clue tiles are explicitly set :

(assert (= V11 10 ))

(assert (= V24 5 ))

(assert (= V47 10 ))

(assert (= V58 6 ))

At the top of the file the type of solver is set to be linear integers.

(set-logic LIA)

(set-option :produce-assignments true)

(set-option :produce-models true)

 At the end of the logic file the results are set for production.

(check-sat)

(get-value (V0 V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 V47 V48 V49 V50 V51 V52 V53 V54 V55 V56 V57 V58 V59 V60 V61 V62 V63 ))

(exit)

The logic file is 642 lines long but is solved in about 0.5 seconds.

The results

For the example puzzle described above, and many others, the logic provides a fully correct answer.

However for a small number of puzzles the logic provides an answer that is mostly correct but includes incorrect, disconnected loops of track. Annoyingly all the examples of solutions with loops are just a few tiles choices away from a fully correct solution. Further research is needed to develop another layer of logic that will eliminate the loops in the solution. Adding more clue tiles would also probably eliminate the loops in the solution.

 

..

 

Round up pyramid number placement from The Turing Tests - Expert Numbers puzzles, solved using SMT (Integer) solver.

 

Page 9 of the Expert Number Puzzle book gives us a straight forward "pyramid of numbers" puzzle to solve. This puzzle is also known as "Sum-up" in some newspapers.

 The answer has the empty circles filled with the value of the two number below added together.

The key to tackling this puzzle is to name each of the circles in an ordered way so that each dependant circles can be easily found. Take the top of the pyramid and name the circle A1,  the next row as B1, B2 and then C1,C2,C3 and on down to the last row E1 to E5. The dependencies are simply generated as .... A1 = B1 + B2.

From this puzzle text file 

#Tri tri_003.txt TTT_p9 Roundup 20250612

x

x,x

x,x,455

x,141,x,x

29,72,x,138,x

A script is used to generate SMT-2 solving input language. This constraint set reads as...

(assert (= A1 (+ B1 B2)))

(assert (= B1 (+ C1 C2)))

(assert (= B2 (+ C2 C3)))

(assert (= C1 (+ D1 D2)))

(assert (= C2 (+ D2 D3)))

(assert (= C3 (+ D3 D4)))

(assert (= D1 (+ E1 E2)))

(assert (= D2 (+ E2 E3)))

(assert (= D3 (+ E3 E4)))

(assert (= D4 (+ E4 E5)))

Before this the variables to be solved, state of the solver and the known circles are declared as ..

(set-logic LIA)

(set-option :produce-models true)

(set-option :produce-assignments true)

(declare-const A1 Int)

(declare-const B1 Int)

(declare-const B2 Int)

(declare-const C1 Int)

(declare-const C2 Int)

(declare-const C3 Int)

(declare-const D1 Int)

(declare-const D2 Int)

(declare-const D3 Int)

(declare-const D4 Int)

(declare-const E1 Int)

(declare-const E2 Int)

(declare-const E3 Int)

(declare-const E4 Int)

(declare-const E5 Int)

and the known values ...... 

(assert (= E4 138 ))

(assert (= E2 72 ))

(assert (= E1 29 ))

(assert (= D2 141 ))

(assert (= C3 455 ))

and finally the answer are requested.

(check-sat)

(get-value ( A1 B1 B2 C1 C2 C3 D1 D2 D3 D4 E1 E2 E3 E4 E5  ))

(exit)

This SMT text file is passed to the solver that replies with 

sat

( (A1 1393)

  (B1 590)

  (B2 803)

  (C1 242)

  (C2 348)

  (C3 455)

  (D1 101)

  (D2 141)

  (D3 207)

  (D4 248)

  (E1 29)

  (E2 72)

  (E3 69)

  (E4 138)

  (E5 110) )

that can be used to generate the final output image. 

Looking at the script, most of the lines are taken up with generating the display and critically checking the answers.  To test the answer checking part of the script a bad value is injected into the answer stream causing this message to appear in the output. The 248 was changed to 284 triggering errors with the C3 and D4 results.

Final comments

The one is about as simple as puzzles get. Interesting the the bottom "E" row appears in the constraint description but are not the target of a specific constraint. Being tied to the values in the "D" row, depending on the clue number placement, different correct results could appear between solvers.  

Both the Mathsat5 and Z3 solvers were able to complete this puzzle using the SMT language as input.