The other day, I was talking to a friend of mine about the Z3 theorem solver and he mentioned the inverted Pyramid puzzle. I told him: “I think this can be solved with Z3” and hence this blog post.
So what’s the inverted pyramid puzzle?
Imagine the following pyramid with 4 rows:
10 9 8 7
6 5 4
3 2
1
The numbers in that triangle are just placeholders for the sake of explanation.
The goal of the puzzle is to find the right order for those numbers in the triangle in such a way that:
For the 4th row, we must have whatever is at the position denoted with [number] subtracted from its neighbor equals the value of the next row’s value beneath the top 2 numbers (note: we take the absolute value of the subtraction). So:
|[10] - [9]| == [6] |[9] - [8] | == [5] |[8] - [7] | == [4]
And for the 3rd row, we must have:
|[6] - [5]| == [3] |[5] - [4]| == [2]
And for the 2nd row, we must have:
|[3] - [2]| == [1]
Of course, we stop at the first row.
For now, here’s a solution for the inverted pyramid with 4 rows:
8 10 3 9
2 7 6
5 1
4
The numbers configuration from above satisfies the conditions explained above.
Please note that the only numbers accepted in the pyramid are [1..Sigma(rows)]. Sigma denotes the sum of the arithmetic series going from 1 to rows.
Solution
To solve this problem, we need to be able to:
- Construct a dummy pyramid with the needed number of rows
- Walk the pyramid and access the slots in questions that we need to do the subtraction operations on.
- Print a pyramid nicely (optional)
- Create the proper Z3 constraints
Steps 1 to 3
If we can achieve step 2, we can leverage Z3 and have it solve this problem for us.
When ROWS is 5, we have Sigma(5) elements, thus 15 elements. So the accepted numbers accepted are 1 to 15 (but we don’t know their proper positioning yet):
15 14 13 12 11
10 9 8 7
6 5 4
3 2
1
To go from ROW=5 to ROW=4, we can deduce that the first element in ROW=4 is Sigma(4), thus 10. Etc.
Our goal is to be able to access slot 15, slot 14 and slot 10. Then, slot 14, slot 13 and slot 9, etc.
To construct the pyramid, we can use this simple comprehension list syntax:
p = list(range(1, sigma(ROWS)+1, 1))
To print the pyramid, we can do:
def print_pyramid(p, R):
"""Display the inverted pyramid"""
p = list(p)
p.reverse()
r = R
indent = 0
max_width = len(str(p[0])) + 1
nb_fmt = "%%%dd " % max_width
for n in p:
if r == 0:
R -= 1
r = R
indent += max_width - 1
print()
print(' ' * indent, end='')
r -= 1
print(nb_fmt % n, end='')
print()
To walk the pyramid and access the needed elements, we can do:
def walk_pyramid(p, R):
"""Walks the pyramid and invokes a callback"""
while R > 0:
base = sigma(R) - 1
next_base = sigma(R-1) - 1
print("*ROW=%d*" % R)
offset = -1
limit = R - 2
while offset < limit:
offset += 1
a = p[base - offset]
b = p[base - offset - 1]
c = p[next_base - offset]
print("|[%d] - [%d]|==[%d]" % (a, b, c))
R -= 1
Step 4 – Using Z3
Now that we know how to create, print and walk the pyramid, we need to use Z3 and give it the proper constraints so it can solve the problem for us.
The solution is implemented in a class for convenience and cleanliness of the code:
class PyramidSolver:
def __init__(self, rows):
self.rows = rows
"""Rows in the pyramid"""
self.data = list(range(1, sigma(ROWS)+1, 1))
"""The actual data (placeholders)"""
self.solver = z3.Solver()
"""The Z3 solver"""
self.syms = {}
"""Symbols for each slot in the pyramid"""
Things to note:
- The unsolved pyramid is stored in the
datamember variable - The Z3 solver is initialized in the
solvermember variable - The symbols dictionary for each slot [1..
Sigma(rows)] is calledsyms
We need to create a Z3 symbol for each slot, for that we use this helper function:
def get_sym(self, n):
"""Returns a new or previous symbol for the position 'n'"""
try:
sym = self.syms[n]
except:
sym = self.syms[n] = z3.Int('n_%d' % n)
return sym
We use a dictionary to map a slot index to a Z3 symbol. It is important to always return the same symbol for the same slot.
Now we can leverage the walk_pyramid function to walk the pyramid and add constraints for us. Instead of printing the numbers, we do the following:
def add_constraints(self, a, b, c):
"""Callback for the walk_pyramid function that creates the proper constraints"""
syms = [get_sym(a), self.get_sym(b), self.get_sym(c)]
solver.add(z3.Or(syms[0] - syms[1] == syms[2], syms[1] - syms[0] == syms[2]))
With this code, we tell Z3 that slot |’a’ – ‘b’| should be equal to slot ‘c’. The a, b, and c denote the two numbers at the top row and single number at the lower row (respectively).
Having walked the whole pyramid, we have created all the basic Z3 constraints.
We are not done yet with the constraints though, we have two more constraints:
- We cannot have repeating numbers
# All symbols are distinct solver.add([z3.Distinct([sym for sym in syms.values()])])
We use Z3’s Distinct to conveniently said that no symbol equals to another. This makes our pyramid with unique numbers
- The numbers should be bounded from [1..
Sigma(rows)]
The final constraint is to tell Z3 that each symbol is bounded:
# All symbols range from 1 to sigma(rows) solver.add([z3.And(s >= 1, s <= len(data)) for s in syms.values()])
We are now ready to ask Z3 to solve this problem and give us a model (one possible solution):
if self.solver.check() != z3.sat:
print("No solution!")
else:
model = solver.model()
for n in syms.keys():
sym = model[self.get_sym(n)] # Get the symbol for slot n
val = sym.as_long() # Get the value for that slot
self.data[n-1] = val # Update the pyramid
If we found a solution (the solver returns sat, then we can get a valid numeric value for each symbol at a given slot and patch them into the data variable (which contains the unsolved pyramid values).
You can find the full solution code on my GitHub: https://github.com/0xeb/puzzles/blob/master/InvertedPyramid/.
That’s it!
You might also like: