Skip to main content
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