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 constrain 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 constrain description but are not he target of a specific constrain. 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.