Doing my Daughter's Homework with the Z3 SMT Solver

Sat 17 October 2020 by A Scented Llama

My nine year old daughter came to me the other day with a difficult math problem. When I looked I realised that she was right - whoever was setting the homework that day hadn’t realised just what they were asking for.

I can’t remember the exact wording but the problem was as follows:

In South African currency, using only bank notes, find all the different ways
you can make R400. How can you be sure you've found all the different
combinations?

I suspect the intention was to use a single note for each combination. In South Africa we have R10, R20, R50, R100 and R200 notes. If we use only a single note each time we get 5 combinations:

40 x R10

20 x R20

8 x R50

4 x R100 and

2 x R200

Stated that way this would indeed be appropriate for a Grade 3 child. However it was not stated like that and the question wanted all possible combinations. I thought about it for a moment and realised that far from being an easy question I actually didn’t know how to go about solving this!

Z3 to the Rescue

For some work research I’ve been playing around with Microsoft’s Z3 Theorem Prover recently. It’s a fascinating piece of software - it’s meant to solve Satisfiability problems. A Satisfiability problem is one where we are given a set of constraints and we need to find some solution that satisfies those constraints. The basic form of this is the Boolean Satisfiability Problem (often just called SAT) where we need to satisfy boolean constraints, which are basically constraints that limit you to true/false propositions. Z3, however, is an SMT solver which stands for Satisfiability Modulo Theorems. That might sound complicated but what it means is simply that instead of just allowing true/false constraints it can also allow theories which can be used to solve other types of constraints. There’s a reason we call them ‘theories’ but I’m not going to get into it. Rather let’s see how we can use Z3 to do my daughter’s homework for her.

Finding our Constraints

We can install Z3 with the typical Python incantation:

pip3 install z3

Once it’s installed a moment’s thought should lead us to the following: what we are really looking for are integer solutions to the equation:

10x + 20y + 50z + 100v + 200w = 400

We have five variables - one for each note type. Z3 comes with some handy Python bindings so let’s use them:

from z3 import *

x = Int('x')
y = Int('y')
z = Int('z')
v = Int('v')
w = Int('w')

solver = Solver()
solver.add(x*10 + y*20 + z*50 + v*100 + w*200 == 400)

We’ve declared 5 variables. We need to use the special Int declaration from Z3 so it knows that those particular variables are constrained to only be integers. Z3 has a number of different variable types but this is all we need for now. We then create a solver and add our constraint. You’ll notice that it’s very easy to express the constraint directly - the Python bindings provide overloaded operators to simplify things.

Another small helper is Ints which takes a list of variables and returns a Z3 Int for each one:

x, y, z, v, w = Ints('x y z v w')

Let’s try and solve our problem. We ask Z3 to check our constraints. If it can find a solution it’ll return a special constant: sat.

print(solver.check())

If we run this code we’ll see the ‘sat’ output which means that Z3 can find a solution. We can ask Z3 what this solution is by finding the model that satisfies the constraints.

model = solver.model()
print(model)

If we print the model we’ll get the following:

[w = 0, z = 0, v = 0, y = 0, x = 40]

Z3 found that 40 tens will satisfy our requirements.

Getting All The Solutions

That’s all good and well and if we only needed one solution we’d be done. However we need to find all the solutions. How do we get Z3 to list them all?

Well - we simply add our new solution as a constraint! This forces Z3 to find some other solution. We can loop through results by checking that we’re still satisfiable and stop the moment Z3 gives up and says it can’t find anymore solutions.

while solver.check() == sat:
    model = solver.model()
    print(model)
    # Note: we can get the value the model assigns to a variable
    # by simply indexing the model with the variable: 
    solver.add(Or(x != model[x],
                  y != model[y],
                  z != model[z],
                  v != model[v],
                  w != model[w]))

We need to be careful here. We can’t simply add, say, x != 20 as a constraint. That would mean we can never assign 20 to x again. But there are multiple solutions where x == 20. We need to make sure all values of a particular solution are constrained at the same time. In order to make sure a solution cannot be used we use the Z3 Or operator. Why the Or operator and not And? Remember that Z3 is going to test each constraint and throw out solutions that don’t satisfy them. If we say, for example, that x != 0 and y != 0 then any solution with an x == 0 or y == 0 won’t satisfy that condition. We’re right back to over-limiting our solution space.

Instead if we add an Or constraint and consider x != 0 or y != 0 then we’re allowed to set x == 0 as long as we don’t set y == 0 as well. So if we use an Or constraint for all the values in our model then only that specific solution will be excluded. This type of thing takes getting used to.

We’re almost ready to count our solutions but there is one more problem. If we run the code as it stands now Z3 runs forever! How is this possible? Can there really be infinite solutions? Well - yes. Consider a solution with three R200 notes. Since that makes R600 we need to take away R200 to get a solution and Z3 will happily assign -2 to our R100 notes. We need to constrain our variables to only positive integers. The And operator works well for this case.

So our full solution is:

from z3 import *

x, y, z, v, w = Ints('x y z v w')

solver = Solver()
solver.add(x*10 + y*20 + z*50 + v*100 + w*200 == 400)
solver.add(And(x >= 0, y >= 0, z >= 0, v >= 0, w >= 0))

solutions = 0
while solver.check() == sat:
    solutions += 1
    model = solver.model()
    print(model)
    # Note: we can get the value the model assigns to a variable
    # by simply indexing the model with the variable: 
    solver.add(Or(x != model[x],
                  y != model[y],
                  z != model[z],
                  v != model[v],
                  w != model[w]))
print(solutions)

And, after all that, we have our answer: there are 236 possibilities.

Can we Solve it Analytically?

After discussing the problem and why it was so difficult with my daughter I printed out the solutions for her and told her that she could state she knew there were no other solutions because we had found them all. Apparently in class the teacher simply ignored the second half of the question and was happy to mark any combinations found by the students as correct. Ce la vie.

This did make me wonder though - can we solve this analytically? Again we need integer solutions to

10x + 20y + 50z + 100v + 200w = 400

My research led me to the fact that this is, apparently, a Linear Diophantine Equation. From what I can see there is no simple formula to give us the number of solutions. There are algorithms to find solutions and they can be used in the same way we used Z3 - to iterate over all possible solutions so we can count them.

I mentioned this all to my wife and her only comment was that she was happy that I’d finally managed to get a Grade 3 question right!