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 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.

 

..