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
No comments:
Post a Comment