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

I had a book gifted that really fits right in my wheelhouse. The book The Turing Tests - Expert Numbers puzzles, has a large collection of puzzles ripe for solving.

The first one is find the arrangement of a standard set of dominoes to cover the pattern provided, with one clue piece already placed.

 

Domino placement puzzle 

A standard set of domino tiles are 28 rectangular tiles with two numbers on each tile. The tiles are:

0-0 0-1 0-2 0-3 0-4 0-5 0-6 1-1 1-2 1-3 1-4 1-5 1-6 2-2 2-3 2-4 2-5 2-6 3-3 3-4 3-5 3-6 4-4 4-5 4-6 5-5 5-6 6-6

 A suitable text encoding of the puzzle looks like:

#dp 0-6 dp_001.txt TTT P7
xxxx66
xxx0421
xxx6356
x00116541
0326105431
0215252430
x22130544
xxx6346
xxx4353
xxxx25
-
6-4,73-83

The encoding of the clue hints at how the problem is broken down for solving. A square numbered grid (0 to 99 in 10 lines) is used to represent the placement board with each tile covering two adjacent cells. Each tile end has a non-unique number but each tile pair is unique and the ends must be in adjacent cells. To solve the puzzle a grid square number must be found for each end of all the tiles.  The tactic is to solve for each end of each tile as a separate value but limited to the places it's allowed in the layout grid.

The logic of the puzzle falls out as :

• Each domino tile is an adjacent pair of non-unique numbers in the range 0-6,
• All tiles must be placed once and once only,
• No tile can overlap another or have a gaps in the final arrangement, but not all squares of the 10*10 grid are used.
• A clue piece is provided.

Moving to the formal language of the SMT solver this becomes :

1. Declaration of 56 integer variables, one for the position of each end of all the tiles,
2. Setting of the 2 clue results,
3. Making sure that each tile end sits on it's own square,
4. Limit each tile end (variable) to only those squares on the provided layout diagram that match. The 0s can only go on a 0 square, 1s on 1 etc.
5. Make sure that both ends of a tile sit on adjacent squares.
6. Set the solver into integer mode and 
7. Retrieve the results.

The perl reframing script does these mundane tasks from reading the input encoding and generating these parts for the list above:  (ignore the line numbering)

5. Set the Solver into integer mode and make it generate values

  1 (set-logic LIA)

  2 (set-option :produce-models true)

  3 (set-option :produce-assignments true)  

1. Declare the variable to hold the board square values as answers.  The [0-0] tile is the two variable V00_00 and V00_10, the [5-6] tile is V50-06 and V50_16.

  4 (declare-const V00_00 Int)

  5 (declare-const V00_10 Int)

  6 (declare-const V00_01 Int)

  7 (declare-const V00_11 Int)

  8 (declare-const V00_02 Int)

  9 (declare-const V00_12 Int)

 10 (declare-const V00_03 Int)

 11 (declare-const V00_13 Int)

 12 (declare-const V00_04 Int)

 ......snip

 55 (declare-const V50_15 Int)

 56 (declare-const V50_06 Int)

 57 (declare-const V50_16 Int)

 58 (declare-const V60_06 Int)

 59 (declare-const V60_16 Int)

 2. Set to two known clue values

 60 (assert (= V40_06 83 ))

 61 (assert (= V40_16 73 ))

 3. Each variable representing the value of one tile end must have a unique answer, being the grid square it will sit on.

 62 (assert (distinct V00_00 V00_10 V00_01 V00_11 V00_02 V00_12 V00_03 V00_13 V00_04 V00_14 V00_05 V00_15 V00_06 V00_16 V10_01 V10_11 V10_02 V10_12 V10_03 V10_13 V10_04 V10_14 V10_05 V10_15 V10_06 V10_16 V20_02 V20_12 V20_03 V20_13 V20_04 V20_14 V20_05 V20_15 V20_06 V20_16 V30_03 V30_13 V30_04 V30_14 V30_05 V30_15 V30_06 V30_16 V40_04 V40_14 V40_05 V40_15 V40_06 V40_16 V50_05 V50_15 V50_06 V50_16 V60_06 V60_16  ))

 4. Each variable must only have the answer that match its face value number.  In the layout grid the 0 appears in 7 squares 13, 31, 32, 40, 45, 50, 59, 65. Therefore we must force each of the variables that has a face number 0 to be one of these grid square values.

 63 (assert (or (= V00_00 13) (= V00_00 31) (= V00_00 32) (= V00_00 40) (= V00_00 45) (= V00_00 50) (= V00_00 59) (= V00_00 65) ))

 64 (assert (or (= V00_01 13) (= V00_01 31) (= V00_01 32) (= V00_01 40) (= V00_01 45) (= V00_01 50) (= V00_01 59) (= V00_01 65) ))

 65 (assert (or (= V00_02 13) (= V00_02 31) (= V00_02 32) (= V00_02 40) (= V00_02 45) (= V00_02 50) (= V00_02 59) (= V00_02 65) ))

 66 (assert (or (= V00_03 13) (= V00_03 31) (= V00_03 32) (= V00_03 40) (= V00_03 45) (= V00_03 50) (= V00_03 59) (= V00_03 65) ))

 67 (assert (or (= V00_04 13) (= V00_04 31) (= V00_04 32) (= V00_04 40) (= V00_04 45) (= V00_04 50) (= V00_04 59) (= V00_04 65) ))

 68 (assert (or (= V00_05 13) (= V00_05 31) (= V00_05 32) (= V00_05 40) (= V00_05 45) (= V00_05 50) (= V00_05 59) (= V00_05 65) ))

...snip

116 (assert (or (= V50_16 4) (= V50_16 5) (= V50_16 23) (= V50_16 26) (= V50_16 35) (= V50_16 43) (= V50_16 73) (= V50_16 76) ))

117 (assert (or (= V60_06 4) (= V60_06 5) (= V60_06 23) (= V60_06 26) (= V60_06 35) (= V60_06 43) (= V60_06 73) (= V60_06 76) ))

118 (assert (or (= V60_16 4) (= V60_16 5) (= V60_16 23) (= V60_16 26) (= V60_16 35) (= V60_16 43) (= V60_16 73) (= V60_16 76) ))

 5. Both of the tile ends must be within 1 square of each other end.  The values in the variables V10_06 V10_16 represents each end of the [0-6] tile and must be only one grid square away from each other. East-west separation is 1 grid square North-South is 10 grid squares.

119 (assert ( or (= 1 (- V00_00 V00_10)) (= 1 (- V00_10 V00_00)) (= 10 (- V00_00 V00_10)) (= 10 (- V00_10 V00_00)) )) ; pair 0 0 ~ V00_00 V00_10

120 (assert ( or (= 1 (- V00_01 V00_11)) (= 1 (- V00_11 V00_01)) (= 10 (- V00_01 V00_11)) (= 10 (- V00_11 V00_01)) )) ; pair 0 1 ~ V00_01 V00_11

121 (assert ( or (= 1 (- V00_02 V00_12)) (= 1 (- V00_12 V00_02)) (= 10 (- V00_02 V00_12)) (= 10 (- V00_12 V00_02)) )) ; pair 0 2 ~ V00_02 V00_12

122 (assert ( or (= 1 (- V00_03 V00_13)) (= 1 (- V00_13 V00_03)) (= 10 (- V00_03 V00_13)) (= 10 (- V00_13 V00_03)) )) ; pair 0 3 ~ V00_03 V00_13

123 (assert ( or (= 1 (- V00_04 V00_14)) (= 1 (- V00_14 V00_04)) (= 10 (- V00_04 V00_14)) (= 10 (- V00_14 V00_04)) )) ; pair 0 4 ~ V00_04 V00_14

124 (assert ( or (= 1 (- V00_05 V00_15)) (= 1 (- V00_15 V00_05)) (= 10 (- V00_05 V00_15)) (= 10 (- V00_15 V00_05)) )) ; pair 0 5 ~ V00_05 V00_15

.... snip

143 (assert ( or (= 1 (- V40_06 V40_16)) (= 1 (- V40_16 V40_06)) (= 10 (- V40_06 V40_16)) (= 10 (- V40_16 V40_06)) )) ; pair 4 6 ~ V40_06 V40_16

144 (assert ( or (= 1 (- V50_05 V50_15)) (= 1 (- V50_15 V50_05)) (= 10 (- V50_05 V50_15)) (= 10 (- V50_15 V50_05)) )) ; pair 5 5 ~ V50_05 V50_15

145 (assert ( or (= 1 (- V50_06 V50_16)) (= 1 (- V50_16 V50_06)) (= 10 (- V50_06 V50_16)) (= 10 (- V50_16 V50_06)) )) ; pair 5 6 ~ V50_06 V50_16

146 (assert ( or (= 1 (- V60_06 V60_16)) (= 1 (- V60_16 V60_06)) (= 10 (- V60_06 V60_16)) (= 10 (- V60_16 V60_06)) )) ; pair 6 6 ~ V60_06 V60_16

 7. Complete the logic lines and request the results

147 (check-sat)

148 (get-value ( V00_00 V00_10 V00_01 V00_11 V00_02 V00_12 V00_03 V00_13 V00_04 V00_14 V00_05 V00_15 V00_06 V00_16 V10_01 V10_11 V10_02 V10_12 V10_03 V10_13 V10_04 V10_14 V10_05 V10_15 V10_06 V10_16 V20_02 V20_12 V20_03 V20_13 V20_04 V20_14 V20_05 V20_15 V20_06 V20_16 V30_03 V30_13 V30_04 V30_14 V30_05 V30_15 V30_06 V30_16 V40_04 V40_14 V40_05 V40_15 V40_06 V40_16 V50_05 V50_15 V50_06 V50_16 V60_06 V60_16  ))

149 (exit)

Working within the constrains of the logic lines above the solver determines a grid square value for each end of each tile. These are returned in the format :

sat

( (V00_00 31)

  (V00_10 32)

  (V00_01 59)

  (V00_11 49)

  (V00_02 50)

...... snip

 (V50_15 85)

  (V50_06 36)

  (V50_16 26)

  (V60_06 4)

  (V60_16 5) ) 

A second invocation of the preparation script reads these results alongside rereading the input puzzle to prepare an html output table. Check are done to ensure each grid square is only used once and both tile ends sit next to each other.  A longer picture should make this all clear showing the encoded puzzle, the grid numbering and the solution as coloured and excel versions.

Final Comments 

This puzzle was similar to the previously solved Gogen puzzle but having two ended tiles rather than single letters to place was an interesting twist. Some time was taken trying to get unique colours for the output picture included above.

The command pipeline to solve runs for about 0.34 elapsed seconds (on a Mac studio ) including generating the output html file.

 % time ./domPlace_smt.pl < dp_001.txt | ../../solver_mathsat5 | ./domPlace_smt.pl -f dp_001.txt > z.html

./domPlace_smt.pl < dp_001.txt  0.01s user 0.00s system 87% cpu 0.012 total

../../solver_mathsat5  0.31s user 0.02s system 98% cpu 0.334 total

././domPlace_smt.pl -f dp_001.txt > z.html  0.01s user 0.00s system 3% cpu 0.334 total

The approach of solving for each end of a tile was seen as less complex than trying to solve of placement and orientation of each domino as a whole. Adding the extra constraint that the two ends of the tile must be next to each other and using creative variable naming completed the excersize.

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