Year: 2018

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:

• Dennis Yurichev – SAT/SMT by example
• Short jokes about the genders and sexuality
• Joke: Jesus saves