Category: Puzzles

Posted on

The inverted pyramid puzzle

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. Continue reading “The inverted pyramid puzzle”

Posted on

Can you solve this puzzle?

I got this silly puzzle via chain mail:

Can you solve it?

Maybe you will be able to, but don’t beat yourself up if you don’t get it right.

You might also like:

Posted on

Riddle: How many brothers and sisters are there in this family? Z3 Theorem prover

The other day, I ran into a riddle:

A brother said to his sister: “I have as many sisters as brothers”
His sister replied: “I have twice as many brothers as I have sisters”

How many brothers and sisters exist in this family?

I figured that it’s a nice exercise for the Z3 theorem prover. All I had to do is express the riddle in a series of constraints and ask Z3 to try to find a solution.

The following is a Z3Py program that expresses the riddle:

import z3

# Create a solver instance
s = z3.Solver()

# Create two variables representing the total number of males and females (m and f)
m, f = z3.Ints('m f')

# The brother said: I have as many brothers as sisters
s.add(m - 1 == f)

# The sister said: I have twice as much brothers as I have sisters
s.add(2 * (f - 1) == m)

# Check for the solution
if s.check() == z3.sat:
  sol = s.model()
  print "Brothers: %d, Sisters: %d" % (sol[m].as_long(), sol[f].as_long())

When we run the solver, we get the following solution: 4 males, 3 females.

If you prefer the good old systems of equations, we can solve it like this:

The brother said:
m - 1 = f          (1)

The sister said:
2 * (f - 1) = m    (2)


So we have 2 equations, let's do some substitution:

-> f = m - 1        (1)
-> 2f - 2 = m       (2)

--> m = 2f - 2      (2)
--> f = 2f - 2 - 1  (1)
--> f = 2f - 3
--> f - 2f = -3
--> -f = -3
--> f = 3

--> m = 2f - 2
--> m = 2*3 - 2
--> m = 6 - 2
--> m = 4

 

You might also like: