Skip to main content
This quickstart guide will help you install Z3 and solve your first constraint problem. By the end, you’ll have Z3 running and understand the basics of SMT solving.

​
What you’ll build

You’ll create a simple Python script that uses Z3 to solve a system of constraints. The solver will find values for variables that satisfy all constraints simultaneously.
1

Install Z3

The easiest way to get started is to install Z3 via a package manager. Choose your preferred language:
Install the Python bindings using pip:
pip install z3-solver
This installs both the Z3 library and Python bindings.
For other installation methods, including building from source, see the installation guide.
2

Write your first Z3 program

Create a file called first_solve.py with the following code:
first_solve.py
from z3 import *

# Create symbolic variables
x = Real('x')
y = Real('y')

# Create a solver instance
s = Solver()

# Add constraints
s.add(x + y > 5)  # x + y must be greater than 5
s.add(x > 1)      # x must be greater than 1
s.add(y > 1)      # y must be greater than 1

# Check if constraints are satisfiable
print(s.check())

# Get a model (solution)
print(s.model())
This program:
  1. Creates two real-valued variables x and y
  2. Adds constraints that define valid values
  3. Checks if the constraints can be satisfied
  4. Prints a model showing values that satisfy all constraints
3

Run the program

Execute your script:
python first_solve.py
You should see output like:
sat
[y = 2, x = 4]
The output sat means the constraints are satisfiable. The model shows one possible solution: x = 4 and y = 2. Note that 4 + 2 > 5, 4 > 1, and 2 > 1, so all constraints are satisfied.
4

Experiment with unsatisfiable constraints

Try adding a conflicting constraint to see what happens when no solution exists:
from z3 import *

x = Real('x')
y = Real('y')
s = Solver()

s.add(x + y > 5)
s.add(x > 1)
s.add(y > 1)
s.add(x + y < 3)  # Conflicts with x + y > 5

result = s.check()
print(result)

if result == sat:
    print(s.model())
else:
    print("No solution exists!")
This will output:
unsat
No solution exists!
The solver correctly identifies that no values can satisfy both x + y > 5 and x + y < 3 simultaneously.
5

Try a logic puzzle

Let’s solve a more interesting problem: the classic Socrates syllogism.
socrates.py
from z3 import *

# Declare a sort (type) for objects
Object = DeclareSort('Object')

# Declare predicates
Human = Function('Human', Object, BoolSort())
Mortal = Function('Mortal', Object, BoolSort())

# Declare Socrates as a constant of type Object
socrates = Const('socrates', Object)

# Variables for quantifiers must be declared as Const
x = Const('x', Object)

# Add axioms
s = Solver()
s.add(ForAll([x], Implies(Human(x), Mortal(x))))  # All humans are mortal
s.add(Human(socrates))  # Socrates is human

# Check if axioms are consistent
print("Axioms consistent:", s.check())

# Try to prove Socrates is mortal (via refutation)
s.add(Not(Mortal(socrates)))
result = s.check()

if result == unsat:
    print("Proved: Socrates is mortal")
else:
    print("Could not prove Socrates is mortal")
Output:
Axioms consistent: sat
Proved: Socrates is mortal
This demonstrates proof by refutation: we prove Socrates is mortal by showing that assuming the opposite (Socrates is not mortal) leads to unsatisfiability.

​
Understanding the results

Z3 returns one of three results:

sat

Constraints are satisfiable. A model (solution) is available.

unsat

No solution exists. The constraints are contradictory.

unknown

The solver couldn’t determine satisfiability (usually due to timeouts or resource limits).

​
Common patterns

Here are some patterns you’ll use frequently:

​
Declaring variables

x = Int('x')
y = Int('y')

​
Adding constraints

s = Solver()

# Arithmetic
s.add(x + y == 10)
s.add(x * 2 > y)

# Boolean logic
s.add(Or(a, b))
s.add(Implies(a, Not(b)))

# Comparisons
s.add(x >= 0)
s.add(y < 100)

​
Checking and retrieving models

result = s.check()

if result == sat:
    m = s.model()
    print(f"x = {m[x]}")
    print(f"y = {m[y]}")
elif result == unsat:
    print("No solution")
else:
    print("Unknown")

​
Next steps

Now that you’ve solved your first problems with Z3, explore these resources:

Core concepts

Learn about SMT solving, expressions, and solvers

Python API

Comprehensive guide to the Python bindings

Examples

Browse practical examples and tutorials

Optimization

Learn how to optimize objectives with Z3
If you encounter import errors, make sure Z3 is installed in your current Python environment. You can verify with pip list | grep z3.

Build docs developers (and LLMs) love

Get started for freeTalk to us