A recent article came up recently and it’s a great way to start using Z3, a popular, general purpose constraint solver (among many things). The article comes with a video workshop and it is a nice supplement.
It’s quite hard to figure out what this kind of solver can be useful for. I tried to read SMT by Example in the past, but it was too much for a start. The above link was an easier intro that gave me a broad overview of the possibilities.
This article shares some problems I liked (mostly ressource allocations and riddles, though Z3 can do much more) and how to solve them using Z3.
I stole some problems in the aforementionned articles, as well as on hakank.org. But ! I spent some evenings typing the solutions or attempting to solve them myself. It felt super hard at first, because that’s a very unusual way to think about problems. What struck me the most (and it especially visible on Einstein’s riddle I think) is that solving the problem is mostly about properly stating it.
Regarding real-life use, I’ve been quite impressed to read things on:
A couple intro problems in order to get used to the syntax and what solving a problem with Z3 looks like.
Let’s start with a short riddle:
9 animals, rabbits and pheasants are playing on the grass. We can see 24 legs. How many rabbits and pheasants are there?
It looks like a system of 2 equations with 2 unknowns, so we can solve by hand or use a equation solver, like scipy.linalg.solve to find a solution. Let’s do this:
# rabbits-pheasans-scipy.py
import numpy as np
from scipy import linalg
a = np.array([[1, 1], [4, 2]])
b = np.array([9, 24])
print(linalg.solve(a, b))
The results are:
python3 rabbits-pheasants-scipy.py
[3. 6.]
We’ve lost what is what but hey, that’s a first result and it only took 5 lines of code.
It turns out Z3 can do this too with another approach. Let’s create the 2 integer parameters (rabbits and pheasants) that will hold the possible values, pop a Solver, add some constraints on our parameters and see if Z3 can come up with a model that matches all the constraints:
# rabbits-pheasans-z3.py
from z3 import *
rabbits, pheasants = Ints("rabbits pheasants")
s = Solver()
s.add(rabbits + pheasants == 9)
s.add(4*rabbits + 2*pheasants == 24)
s.check()
print(s.model())
Now we can run it:
python3 rabbits-pheasans.py
[pheasants = 6, rabbits = 3]
We’ve found the same results, great! The code may look similar, but the two approaches are very different: with Z3, we are not creating matrixes or unknowns and equations. We are creating parameters on top of which we add constraints, and we want to find a model that matches those constraints.
There are 2 drawbacks to using an ad hoc solution :
The riddle could have been:
9 animals, rabbits and pheasants are playing on the grass. We can see 24 legs, or maybe was it 27 ? How many rabbits and pheasants are there?
This is still very easy to solve by hand, but from a mathematical point of view with an equation solver it becomes more complex:
With Z3, all we have to do is add an Or clause:
# rabbits-pheasans-z3.py
from z3 import *
rabbits, pheasants = Ints("rabbits pheasants")
s = Solver()
s.add(rabbits + pheasants == 9)
s.add(Or(
4*rabbits + 2*pheasants == 24,
4*rabbits + 2*pheasants == 27))
s.check()
print(s.model())
On to something a bit more complex.
Einstein’s riddle goes like this:
Now, who drinks water? Who owns the zebra?
It takes some time to solve by hand. It took me 25 minutes with Z3. Most of them were used to correctly identify the known values and type the constraints. Look at how simple the code is !
from z3 import *
nationalities = Ints("Englishman Spaniard Ukrainian Norwegian Japanese")
cigarettes = Ints("Parliaments Kools LuckyStrike OldGold Chesterfields")
animals = Ints("Fox Horse Zebra Dog Snails")
drinks = Ints("Coffee Milk OrangeJuice Tea Water")
house_colors = Ints("Red Green Ivory Blue Yellow")
parameter_sets = [nationalities, cigarettes, animals, drinks, house_colors]
Englishman, Spaniard, Ukrainian, Norwegian, Japanese = nationalities
Parliaments, Kools, LuckyStrike, OldGold, Chesterfields = cigarettes
Fox, Horse, Zebra, Dog, Snails = animals
Coffee, Milk, OrangeJuice, Tea, Water = drinks
Red, Green, Ivory, Blue, Yellow = house_colors
solver = Solver()
for parameter_set in parameter_sets:
# We want all the values for a given category:
# - to be different
solver.add(Distinct(parameter_set))
# - to be between 1 and 5 included
for parameter in parameter_set:
solver.add(parameter >=1, parameter <= 5)
def Neighbor(a, b):
"""A z3 constraints that states that a is a neighbor of b"""
return Or(a == b + 1, a == b - 1)
solver.add(Englishman == Red)
solver.add(Spaniard == Dog)
solver.add(Coffee == Green)
solver.add(Ukrainian == Tea)
solver.add(Green == Ivory + 1)
solver.add(OldGold == Snails)
solver.add(Kools == Yellow)
solver.add(Milk == 3)
solver.add(Neighbor(Chesterfields, Fox))
solver.add(Neighbor(Kools, Horse))
solver.add(LuckyStrike == OrangeJuice)
solver.add(Japanese == Parliaments)
solver.add(Neighbor(Norwegian, Blue))
solver.check()
m = solver.model()
# Result display
houses = []
for i in range(1, 5+1):
house = []
for parameter_set in parameter_sets:
p = list(filter(lambda x: m.eval(x) == i, parameter_set))[0]
house.append(p)
houses.append(house)
# formatting the result is inspired by what peter norvig for its sudokus:
# http://norvig.com/sudoku.html
max_width = max(len(str(p)) for parameter_set in parameter_sets for p in parameter_set)
for r in range(0, 5):
print(''.join(str(houses[r][c]).center(max_width)+('|' if c < 4 else '') for c in range(0, 5)))
It turns out the englishman owns a zebra and drinks water:
python3 einstein.py
Spaniard | LuckyStrike | Dog | OrangeJuice | Ivory
Norwegian | OldGold | Snails | Coffee | Green
Japanese | Parliaments | Horse | Milk | Blue
Ukrainian | Kools | Fox | Tea | Yellow
Englishman |Chesterfields| Zebra | Water | Red
I’ve liked to solve XKCD 287 because, well, I like XKCD, but also mostly because it’s always a pleasure to overengineer a solution to a seemingly simple problem.
from z3 import *
# https://xkcd.com/287/
prices = [215, 275, 335, 355, 420, 580]
appetizers = [
"Mixed fruits",
"French Fries",
"Side Salad",
"Hot Wings",
"Mozzarella Sticks",
"Sampler Plate"
]
total = 1505
quantities = [Int(f"q_{i}") for i in range(len(appetizers))]
solver = Solver()
for i in range(len(appetizers)):
# We know add the quantities must be below 10
solver.add(quantities[i] >= 0, quantities[i] <= 10)
solver.add(total == Sum([q*p for (q,p) in zip(quantities, prices)]))
# Then we explore the solutions
nb_solutions = 0
while solver.check() == sat:
nb_solutions+=1
m = solver.model()
print(f"# Solution {nb_solutions}")
qs = [m.eval(quantities[i]) for i in range(len(appetizers))]
for i in range(len(appetizers)):
if qs[i].as_long() > 0:
print(qs[i], appetizers[i], m.eval(qs[i]*prices[i]))
# When a solution is found, we add another constraint: we don’t want to find this solution again
solver.add(Or([quantities[i] != qs[i] for i in range(len(appetizers))]))
print()
In this instance, we explore the multiple solutions, by adding extra constraints after each run.
Here are the solutions:
# Solution 1
7 Mixed fruits 1505
# Solution 2
1 Mixed fruits 215
2 Hot Wings 710
1 Sampler Plate 580
Those are not real-life problems (though to some extent they could be), but understanding those small problems is a great introduction to doing more complex things.
Here is a scenario that could be a real life problem of some sort. In this instance, we do not use a Solve, but an Optimizer in order to minimize a quantity.
You have skis of different sizes, and skiers that want to rent your skis.
Your objective is to find an assignment of skis to skiers that minimizes the sum of the disparities between ski sizes and skier heights.
Here are some sample data:
- Ski sizes: 1, 2, 5, 7, 13, 21.
- Skier heights: 3, 4, 7, 11, 18.
I stole this problem here. In a different style, Secret Santa was cool too.
from z3 import *
# we need to turn our python array into z3 arrays in order to compute the sum of the absolute values of the disparities
# https://stackoverflow.com/a/52720429
def create_z3_array(solver, name, data):
a = Array(name, IntSort(), IntSort())
for offset in range(len(data)):
solver.add(a[offset] == data[offset])
return a
def AbsZ3(a):
"""Compute the absolute value of A, as a z3 constraint"""
return If(a < 0, -a, a)
skis = [1, 2, 5, 7, 13, 21]
skiers = [11, 3, 18, 4, 7]
solver = Optimize()
skis_a = create_z3_array(solver, "skis", skis)
skiers_a = create_z3_array(solver, "skiers", skiers)
# This list will map the skis we give to each skier
assignments = [Int(f"skis_for_skiers_{i}") for i in range(len(skiers))]
# We want everybody to have different skies
solver.add(Distinct(assignments))
# We want the assignment to be to existing skis
for a in assignments:
solver.add(a >= 0, a < len(skis))
# Then, we want to compute the disparities, as the sum of the absolute differences of heights between skiers and skis
disparities = Int("disparities")
solver.add(disparities == Sum([AbsZ3(skiers_a[i] - skis_a[assignments[i]]) for i in range(len(skiers))]))
# We want to minimize this quantity
solver.minimize(disparities)
# Then we get the results
solver.check()
m = solver.model()
for i in range(len(assignments)):
print("Skier {} measures {} and will takes the skis of height {} (difference {})".format(
i,
skiers[i],
m.eval(skis_a[assignments[i]]),
m.eval(Absz3(skis_a[assignments[i]] - skiers_a[i]))))
Here is a new problem:
Your day starts at 9 and finishes at 17.
You have 4 tasks to do today, all with different durations:
- work (4 hours)
- send some mail (1 hour)
- go to the bank (4 hours)
- do some shopping (1 hours)
One task has to be finished before you start another. Additionnally, you have to:
- send the mail before going to work
- go to the bank before doing some shopping
- start work after 11
How do you organize your day ?
This is easy to do by hand (in fact you probably do this kind of things in your head for yourself already), but also not very hard to program with Z3. The nice thing is that, once you can program this, you can move on to more complex schedules or ressource-ordering problems like :
from z3 import *
solver = Solver()
tasks = Ints("work mail bank shopping")
work, mail, bank, shopping = tasks
durations = {
work: 4,
mail: 1,
bank: 2,
shopping: 1,
}
start_times = { t: Int(f"start_{t}") for t in tasks }
for t in tasks:
# a task must start after 9
solver.add(start_times[t] >= 9)
# a task must be over by 17
solver.add(start_times[t] + durations[t] <= 17)
# A task should be over before another starts:
for t1 in tasks:
for t2 in tasks:
if t1 == t2:
continue
solver.add(Or(
start_times[t1] + durations[t1] <= start_times[t2],
start_times[t2] + durations[t2] <= start_times[t1]
)
)
# Additionnal constraints:
# - start work after 11
solver.add(start_times[work] >= 11)
# - send the mail before going to work
solver.add(start_times[mail] + durations[mail] <= start_times[work])
# - go to the bank before doing some shopping
solver.add(start_times[bank] + durations[bank] <= start_times[shopping])
print(durations)
solver.check()
m = solver.model()
print(m)
print(solver)