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: