Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/Z3Prover/z3/llms.txt

Use this file to discover all available pages before exploring further.

This tutorial introduces the basic concepts of Z3 through simple constraint solving examples. You’ll learn how to create variables, add constraints, and check satisfiability.

​
Simple Arithmetic Constraints

Let’s start with a basic example that solves arithmetic constraints using real numbers.
1

Import Z3

First, import the Z3 library to access all solver functions:
from z3 import *
This imports all Z3 classes and functions, including Real, Solver, and constraint operators.
2

Create variables

Create variables that represent unknown values you want to find:
x = Real('x')
y = Real('y')
Real('x') creates a real-valued variable named ‘x’. Z3 also supports Int, Bool, and other types.
3

Create a solver and add constraints

Create a solver instance and add your constraints:
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
The add() method accepts multiple constraints. Here we’re saying:
  • The sum of x and y must be greater than 5
  • x must be greater than 1
  • y must be greater than 1
4

Check satisfiability and get a model

Ask Z3 to find a solution:
print(s.check())
print(s.model())
The check() method returns:
  • sat - constraints are satisfiable (solution exists)
  • unsat - no solution exists
  • unknown - solver couldn’t determine
If satisfiable, model() returns concrete values that satisfy all constraints.

​
Complete Example

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())
Expected output: 
sat
[y = 2, x = 4]
The actual values may vary - Z3 finds any solution that satisfies the constraints, not necessarily a specific one.

​
Integer Constraints

Z3 can also solve integer programming problems.
1

Create integer variables

from z3 import *

a = Int('a')
b = Int('b')
c = Int('c')
2

Add constraints

s = Solver()
s.add(a + b + c == 10)
s.add(a >= 0, b >= 0, c >= 0)
s.add(a > b)
This finds three non-negative integers that sum to 10, where a is greater than b.
3

Find a solution

if s.check() == sat:
    m = s.model()
    print(f"a = {m[a]}, b = {m[b]}, c = {m[c]}")
else:
    print("No solution found")
Expected output: 
a = 5, b = 0, c = 5

​
Boolean Satisfiability (SAT)

Z3 can solve classic SAT problems using boolean variables. 
from z3 import *

# Create boolean variables
p = Bool('p')
q = Bool('q')
r = Bool('r')

s = Solver()
# Add a CNF formula: (p OR q) AND (NOT p OR r) AND (NOT q OR NOT r)
s.add(Or(p, q))
s.add(Or(Not(p), r))
s.add(Or(Not(q), Not(r)))

if s.check() == sat:
    m = s.model()
    print(f"p = {m[p]}, q = {m[q]}, r = {m[r]}")
Expected output: 
p = True, q = False, r = True

​
Checking Unsatisfiability

Sometimes constraints have no solution: 
from z3 import *

x = Int('x')
s = Solver()

# Contradictory constraints
s.add(x > 10)
s.add(x < 5)

result = s.check()
print(result)  # prints: unsat
Expected output: 
unsat
When check() returns unsat, calling model() will raise an exception since no solution exists.

​
Key Concepts

  • Int('name') - Integer variables
  • Real('name') - Real number variables
  • Bool('name') - Boolean variables
  • BitVec('name', size) - Bit-vector variables
  • Arithmetic: +, -, *, /, %
  • Comparison: ==, !=, <, <=, >, >=
  • Boolean: And(), Or(), Not(), Implies()
  • Special: Distinct() - ensures all arguments are different
  • sat - Satisfiable (solution found)
  • unsat - Unsatisfiable (no solution exists)
  • unknown - Solver timed out or couldn’t determine

​
Next Steps

Sudoku Solver

Apply these concepts to build a complete Sudoku solver

Optimization Problems

Learn to find optimal solutions using Z3’s Optimize solver

Build docs developers (and LLMs) love

Get started for freeTalk to us