A while ago, a friend presented me an optimization problem that he stumbled upon in his day job.
The problem seemed interesting, so I considered writing a program to solve it, though after a while
I decided to let the occassion pass. The thing is, I don’t know that much about optimization and
I had no idea about where to start! Besides, I had tried solvers for linear programming in the past,
but the lack of documentation and difficulties to get them working on Windows were really off-putting.

That was the situation until I came across this article,
where the author explores the world of SAT solvers and comes to the conclusion that they
are criminally underused by the industry. I even read on Hacker News that someone had solved
an Advent of Code puzzle using Z3! While I had heard of Z3 and SAT solvers before, I thought
they were more of a research thing, unsuitable for tackling real-world problems. The article
and the comments on Hacker News suggested that I was wrong. Now I was curious. I had to find out.

This blog post is a report on this adventure, in which I used Z3 to model and solve the problem.
The code is on GitHub, in case you are curious.
Note that, while I mention some of the steps that led me to the final solution, finding the
right way to model the problem involved lots of trial and error. The real process was messier than
this blog post may suggest.

Wait… What is Z3?

From the official tutorial:

Z3 is a state-of-the art theorem prover from Microsoft Research. It can be
used to check the satisfiability of logical formulas over one or more
theories. Z3 offers a compelling match for software analysis and verification
tools, since several common software constructs map directly into supported
theories.

For our purposes, it comes down to the following: if we manage to express our
problem in terms of logical formulas, then we can pass that to Z3 and let it
find a solution to the problem. There is no need to think algorithms… just
the formulas and Z3 magic!

The problem

Imagine you are organizing a cooking workshop. There are i teachers, j
students and k practical assignments. For each practical assignment, students
need to be divided in i groups, so they can work on the assignment under the
supervision of a teacher. There are two additional requirements:

• Every teacher must teach every student at least once
• We want to maximize the amount of students that get to know each other
  during the assignments (i.e. the amount of pairs of students that have worked
  together in at least one assignment)

For instance, with 2 teachers, 6 students and 2 lab assignments, you could get
the following division:

Assignment 1:

• Teacher 1: student 1, student 2, student 3
• Teacher 2: student 4, student 5, student 6

Assignment 2:

• Teacher 1: student 4, student 5, student 6
• Teacher 2: student 1, student 2, student 3

In this example, every teacher has taught every student. However, by necessity
that means that the amount of students that got to know each other is low. In
fact, the groups did not change between assignment 1 and 2, only the teachers
did. Things become much more interesting when the amount of practical
assignments (k) is bigger, but we will stick to this example to keep things
simple.

Failed attempt at using Rust’s bindings for Z3

These days, my programming language of choice for side projects is Rust. I was
happy to find out there are unofficial Z3
bindings for the language. However, when trying
them out, I was not able to get them working. Since I had no previous experience
with the bindings and the documentation was non-existing, I ended up filing an
issue on GitHub and moved on.

Building a custom interface to Z3

Since I really wanted to use Rust for this project, I set out to find a workaround
for the lack of bindings. It turns out that you can use Z3 as a REPL if
to run the binary as z3 -in. This means that you can write a Rust
program that talks to the Z3 REPL under the hood, by piping input to Z3’s stdin
and getting the responses back from Z3’s stdout. A hacky and stringy-typed
approach, but it actually worked quite well.

An unexpected benefit is that I no longer had to use the (undocumented)
bindings. Instead, I could interact with Z3 using the SMT-LIB
language, which is better documented
(as you can see from the tutorial I
mentioned above). After a short while I was solving hello-world-like problems in
Z3, driven by my little Rust program.

Modeling the problem, part 1

As a recap, we have i students, j teachers and k assignments. The first
thing we need to do is to to specify which output we expect from Z3. We want to
know, for each student and assignment, the teacher that is designated as their
supervisor. If you were doing Rust, you could define this as: