Recently I have come across a nice article: Many Hard Leetcode Problems are Easy Constraint Problems, and I figured, I really should learn how to use these things! What else do I really have to do? I have had use for solvers (or as they are commonly called: theorem provers) In a previous article, but then I tried to prove the things with good old algorithms. I looked at z3 at the time, but found the whole concept a bit too opaque. Now however, it seemed a bit easier to get into.
To be clear, as of writing these words, I have only been looking at z3 reading material for two days. I am in no way an expert, and I have not written anything more complex than a solver for the change counter problem (the first example in the article listed above). So I am writing this really knowing nothing about the underlying theory, theorem provers, or whatever the hell "unification" is. There is a good chance you know more about this than I do.
There are z3 bindings in many popular languages. I will be using z3 's Rust bindings, because I am more comfortable in Rust than, say, Python or JavaScript. The examples I worked with to understand z3 however, can be found in two nice documents:
What are Solvers?
Solvers are a class of .. tools? libraries? where you input some rules and constraints and have the tool just .. solve it for you. It is not going to be a faster or more optimized solution than a custom made algorithm, but it is much easier to change the rules on the fly.
There are many real world uses. They are often used for scheduling and resource allocation problems. Consider the common scenario of a school schedule: Mary cannot work on Tuesdays because she needs to take care of her father; John lives far so he cannot give classes before 10; Class 3-A is full of nerds so their math hours are double; city council regulates no outdoor activity after 12; Susan and Sarah hate each other so you should not have them teach the same class; etc. You can either have two teachers work on it for a week, or just pop it in a solver!
The MiniZinc homepage (another popular solver) has a couple of nice examples: a seating chart, rostering, vehicle routing, grid coloring.
On that note, you might wonder: why did I go with z3 when MiniZinc has a more colorful homepage and is actually referenced by the article linked at the start of this article? The answer is because z3 has bindings in Rust. That is pretty much it.
A Note on Terminology
Documentation on z3 and its API use a lot of jargon, which makes the whole thing really difficult to wade into without a previous background. I will explain things as I understand when I get to them, but two things really stand out.
... continue reading