A Dumb Introduction to Z3 (2025)

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/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; John cannot give classes before 10; 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!

A Note on Terminology

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

1. Sort: This is just the jargon word for types. It has nothing to do with sorting.
2. Constants: They are actually the knobs the solvers use to solve problems. There are free constants (variables) and interpreted constants (literals).

Solvers have their own type system. z3 uses a language called "SMT-LIB2" (smt2). Much of what the bindings do is take your code and translate it internally to this language.

A Simple Equation

Let's solve for x: x + 4 = 7. Here is the Rust program to solve it:

use z3::{Solver, ast::Int};
fn main() {
    let solver = Solver::new();
    let x = Int::new_const("x");
    solver.assert((&x + 4).eq(7));
    _ = solver.check();
    let model = solver.get_model().unwrap();
    println!("{model:?}");
}

This prints x -> 3. The variable is declared as a function that evaluates to 3.

A Jump in Complexity

Consider a system of equations:

• x + y = 17
• y = 2 * x

If defined as Int, the solver returns Unsat (Unsatisfiable). If we change the type to Real, it returns Sat (Satisfiable) with rational solutions:

• y -> 34/3
• x -> 17/3

You can extract these values programmatically using approx_f64(), resulting in x: 5.667 and y: 11.333.