A Dumb Introduction to Z3

Z3 is a powerful tool for solving complex logic and constraint problems without custom algorithms. This article introduces Z3 through Rust, aimed at beginners looking to simplify hard computational problems.

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. So I am writing this really knowing nothing about the underlying theory, theorem provers, or whatever the hell "unification" is.

What are Solvers?

Solvers are a class of tools 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; John cannot give classes before 10; Class 3-A needs double math hours; etc. You can either have two teachers work on it for a week, or just pop it in a solver!

A Note on Terminology

Documentation on z3 and its API use a lot of jargon. Two things really stand out:

Sort: This is just the jargon word for types. It has nothing to do with sorting.
Constants: They are actually the knobs the solvers use to solve problems. Free constants are what one would call variables.

Solvers have their own types (sorts) and operations. Much of the code you write is about expressing things in the target solver's language, such as "SMT-LIB2".

A Simple Equation

Let's start with the simplest equation. Solve for x: x + 4 = 7.

Using Rust bindings, you define the variable, assert the equation, and run the solver. The solver finds that x evaluates to 3. Internally, the variable is declared as a function that takes no input and gives an output.

A Jump in Complexity

Solving a system of equations like x + y = 17 and y = 2 * x is just as straightforward. If the solver returns Unsat (Unsatisfiable), it means no integer solution exists. By switching to the Real type, the solver can provide rational solutions like x -> 17/3 and y -> 34/3, which can then be converted to floating-point numbers for programmatic use.