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.

Chat-GPT and other OCR performance tested on grid data.

Chat-gpt OCR fail in June 2025, Excel does better.

 The image above is a Samurai Sudoku that consists of five interlocked normal sudoku. Each of which works using the normal sudoku rules. This puzzle has been solved using SMT integer solvers but the tedious part is typing in the initial puzzle. Extracting the numbers into a matrix seems like the kind of work that would be suitable for AI. Turns out neither AI nor other "free" web OCR offerings are suitable.

Chat-GPT just can't read the grid ( or the numbers )

That was a rather disappointing fail. It seems obvious that the grid has not been correctly removed before extracting the numbers and the alignment of the numbers has not been preserved. There are also numbers missing from the top right hand corner of the puzzle. Refining the ask produces hardly any better results.

We follow up with a refinement ... 

And the results .... It seems a bit like a sulky teenager who knows what work needs to be done but can't actually put in sufficient effort to get correct and accurate results.

The best Chat-gpt managed on two passes

Other "Free OCR" services

After a quick search, a couple of "free" image to OCR services were tried out. Both of these offered to do the conversion work but would not deliver the results until a fee was paid. The fee was often tied up with some kind of subscriptions to the service. Only one service would deliver the results by email but provided this useless file where all the structure of the numbers has been lost.

Excel has the answer (almost)

After a bit of further searching for a solution the following Excel feature was found in this support note with a handy demo video. "Insert data from a picture" This would seem to be the exact answer required until the killjoy text ....

Important: Data from Picture in Excel for Windows is only supported on Windows 11 or Windows 10 version >=1903 (must have Microsoft Edge WebView2 Runtime installed).

However Excel for Office365, being a web platform, was more accommodating even when driven from a Mac. Using Data -> Data from Picture, the image was loaded and examined automatically then choices offered to correct the data. After correction, 1 seemed to be misread, the data was accepted into the sheet.

**Update as of June 2025 with Excel for Mac 16.98 the Data from picture feature is available offering the choice of reading the source picture from file or clipboard. The read from Clipboard was a fail but the read data from file gave similar results than the Office365 method. The OCR Engine may be different so results might vary. **

After some coloured boxed are added, a very presentable and nearly accurate enough looking sheet. Can you see what's wrong ?

Solution

This far down the workflow, it's just a short push to the solution using an SMT integer solver. First some minor changes are required to prepare the input text before exporting as a .csv for use by the solving scripts.

Some "x" gap markers and end of data "z" markers were added to help with the later editing of the exported .csv file.

Once exported the X & Z markers are removed and ,, converted to ,0, using vi text editor commands. After the first pass at solving it becomes clear there is an image to grid transcription error. An extra line has been inserted and some of the data ( 5 then 1 & 2 ) was split between those lines. This may have been caused by the slight tilt in the original image but is not very satisfactory. 

After correcting the misalignment and using the previously described sudoku .csv to SMT integer conversion script Mathsat solver completed the task in  about 0.34 seconds on an M2 Mac.

% time ./sudoku_GiantX_smt2.pl < RG_002.csv | ../../../solver_mathsat5 | ./sudoku_GiantX_smt2.pl -f RG_002.csv > RG_002.html

./sudoku_GiantX_smt2.pl < RG_002.csv  0.01s user 0.01s system 88% cpu 0.021 total

../../../solver_mathsat5  0.34s user 0.02s system 98% cpu 0.369 total

./sudoku_GiantX_smt2.pl -f RG_002.csv > RG_002.html  0.01s user 0.00s system 4% cpu 0.370 total

giving this answer image. 

Mac native method also failed

A Mac native method was suggested but did not go well.

Using photos to find text in an image.

Only the highlighted cells are found and extracted.

Grid format, number order are lost when pasted into Numbers.

In conclusion

Chat GPT did not get anywhere near the required level of accuracy for this relatively simple looking OCR task. Other web based "text extraction from an image" services required upfront payments, even though they said they were free.

Digging deep into the reliable proven, if idiosyncratic, Microsoft Excel found an answer. Even that wasn't perfect with a line split incorrectly in the data. Further refinement of the Excel extraction workflow will probably provide a close enough solution, removing the need to type in the Samurai Sudoku grids. To get the best capture of numbers and positions, as with any OCR process the text should stand out from the background. Using a picture editor to change the background from grey to white helped make the image more readable.

The Mac native "Find text in an image" was also disappointing but as the "data from picture" feature is now available in Excel for Mac, latest versions, this platform can be used.

Reworking the process on a similar image

From the original image after being "de grayed" ...

Original "degray ed" image

Recognised by Excel import from picture becomes ( after a bit of text editing ) ..

In the above text 3 numbers were out of place in the grid, found by manual inspection.
After passing through the translation and solving process becomes

And finally it only seemed fair to give Chat-GPT another go using the cleaned up picture ...

Slightly better on the shape but the contents are all woefully incorrect and over the place.