Z3 Solver — Solving Constraints with SMT

In this tutorial, you'll learn about Z3 Solver. We cover key concepts, practical examples, and best practices to help you understand and apply this topic effectively.

Z3 is a high-performance SMT Solver from Microsoft Research that solves constraint satisfaction problems across multiple theories, from boolean logic to arithmetic, arrays, and bit vectors.

Learning Path

flowchart LR
  A["SAT & SMT Solving"] --> B["Z3 Solver
Solving Constraints"]
  B --> C["Bounded Model Checking"]
  B --> D["Theorem Proving"]
  style B fill:#f90,color:#fff,stroke-width:2px

Prerequisites

Python programming. Basic logic (SAT/SMT fundamentals from earlier tutorials).

What Is Z3?

Z3 solves satisfiability modulo theories — it checks if a formula is satisfiable given background theories. Unlike SAT solvers that only handle propositional logic, Z3 integrates solvers for arithmetic, arrays, bit vectors, strings, and algebraic data types.

Step-by-Step: Basic Z3 Usage

Step 1: Install

pip install z3-solver

Step 2: Boolean Solving

from z3 import Bool, And, Or, Not, Solver, sat

p = Bool("p")
q = Bool("q")
r = Bool("r")

formula = And(Or(p, q), Or(Not(p), r), Or(Not(r), Not(q)))

solver = Solver()
solver.add(formula)
if solver.check() == sat:
    model = solver.model()
    print(f"p = {model[p]}, q = {model[q]}, r = {model[r]}")

Expected output:

p = True, q = False, r = False

Step 3: Integer Arithmetic

from z3 import Int, And, Solver, sat

x = Int("x")
y = Int("y")

formula = And(
    x + y == 10,
    x - y == 2,
    x > 0,
    y > 0
)

solver = Solver()
solver.add(formula)
if solver.check() == sat:
    model = solver.model()
    print(f"x = {model[x]}, y = {model[y]}")

Expected output:

x = 6, y = 4

Step 4: Bit Vectors

Bit vectors model machine integers with precise overflow behavior:

from z3 import BitVec, BitVecVal, Solver, sat

a = BitVec("a", 32)
b = BitVec("b", 32)

solver = Solver()
solver.add(a + b == 100)
solver.add(a > 0, b > 0)
solver.add(a - b == 20)

if solver.check() == sat:
    model = solver.model()
    print(f"a = {model[a]}, b = {model[b]}")

Expected output:

a = 60, b = 40

Step-by-Step: Program Verification with Z3

Step 1: Model a Simple Function

from z3 import *

def verify_mul_by_2():
    x = Int("x")
    y = Int("y")
    # y = x * 2
    spec = And(
        y == 2 * x,
        x >= 0,
        y >= x
    )
    solver = Solver()
    solver.add(Not(spec))
    if solver.check() == unsat:
        print("Property holds for all x >= 0")
    else:
        print("Counterexample found")

verify_mul_by_2()

Expected output:

Property holds for all x >= 0

Step 2: Array Constraints

from z3 import Array, IntSort, Store, Select, Solver, sat

arr = Array("arr", IntSort(), IntSort())
x = Int("x")
y = Int("y")

# arr[x] = y and arr[x] != y should be unsat
formula = And(
    arr[x] == y,
    arr[x] != y
)

solver = Solver()
solver.add(formula)
print(f"Satisfiable: {solver.check()}")

Expected output:

Satisfiable: unsat

Step 3: Optimization with Z3

from z3 import Optimize, Int

x = Int("x")
y = Int("y")

opt = Optimize()
opt.add(x + y == 10)
opt.add(x >= 0, y >= 0)
opt.maximize(x * y)

result = opt.check()
if result == sat:
    model = opt.model()
    print(f"x = {model[x]}, y = {model[y]}, product = {model[x] * model[y]}")

Expected output:

x = 5, y = 5, product = 25

Common Errors

1. Mixing Int and BitVec

Int is mathematical integer (unbounded). BitVec is machine integer (bounded). Operations valid on one may not work on the other.

2. Not Using BitVec for Low-Level Code

For C integer semantics (wrapping overflow), use BitVec. Int cannot model overflow behavior.

3. Quantifier Performance

Quantifiers use heuristic instantiation and may be slow. Prefer quantifier-free formulas where possible.

4. Missing Model Extraction Check

Always verify solver.check() == sat before calling solver.model(). An unsat query raises an exception on model access.

5. Large Bit-Vector Widths

Bit vectors of 64+ bits create large SAT encodings. Use 8 or 16 bits for prototyping.

Practice Questions

Q1: What theories does Z3 support?

Boolean, integer, real, bit vector, array, string, floating-point, algebraic data types, and quantifiers.

Q2: How does Z3 differ from a SAT solver?

Z3 integrates multiple theory solvers with a SAT core. SAT solvers only handle propositional CNF formulas.

Q3: What is the difference between Int and Real in Z3?

Int uses integer arithmetic. Real uses rational arithmetic with infinite precision.

Q4: Can Z3 solve optimization problems?

Yes. Use Optimize() instead of Solver() and call maximize() or minimize() on expressions.

Q5: How do I get all solutions in Z3?

Use a while loop: get a model, add a blocking clause excluding that model, and re-check.

Challenge

Use Z3 to solve a Sudoku puzzle. Model a 9x9 grid with integer variables, add the standard Sudoku constraints (rows, columns, 3x3 boxes all contain 1-9), and find a solution.

FAQ

Built by the developers of Doda Browser, DodaZIP, and Durga Antivirus Pro.