formal-z3-solver-basics

Out of Scope: - Low-level C++ API (use Python bindings) - Custom theory development - Advanced proof engineering (see lean-theorem-proving.md) - SAT-only solving (see sat-solving-strategies.md)

Z3 Solver Basics

Metadata

• Skill ID: z3-solver-basics
• Category: Formal Methods / SMT Solving
• Complexity: Intermediate
• Prerequisites: Python programming, basic logic, constraint satisfaction
• Last Updated: 2025-10-18

Overview

Purpose

Master Z3 SMT solver for constraint solving, program verification, symbolic execution, and optimization problems using the Python API.

Scope

In Scope:

• Z3 Python API fundamentals
• SMT theory selection (QF_LIA, QF_BV, arrays, reals)
• Constraint modeling and encoding
• Solver modes (satisfiability, optimization)
• Tactics and strategies
• Unsat cores and proof extraction

Out of Scope:

• Low-level C++ API (use Python bindings)
• Custom theory development
• Advanced proof engineering (see lean-theorem-proving.md)
• SAT-only solving (see sat-solving-strategies.md)

When to Use This Skill

Primary Use Cases:

• Solving constraint satisfaction problems
• Program verification and bug finding
• Test input generation
• Scheduling and planning problems
• Symbolic execution
• Configuration validation

Choose Z3 When:

• Need theories beyond Boolean (integers, bitvectors, arrays)
• Require optimization (maximize/minimize objectives)
• Want integrated theory reasoning
• Need unsat core extraction
• Prefer Python API for rapid prototyping

Alternatives:

• MiniSat/CryptoMiniSat: Pure Boolean SAT (faster for SAT-only)
• CVC5: Alternative SMT solver with different strengths
• Yices2: Fast for linear arithmetic
• Constraint programming: Use OR-Tools for discrete optimization

Core Concepts

1. SMT Theories Hierarchy

SMT (Satisfiability Modulo Theories)
├── QF_UF (Uninterpreted Functions)
├── QF_LIA (Linear Integer Arithmetic)
├── QF_LRA (Linear Real Arithmetic)
├── QF_BV (Bitvectors)
├── QF_AUFLIA (Arrays + UF + Linear Integer Arithmetic)
├── QF_AUFBV (Arrays + UF + Bitvectors)
└── Non-quantifier-free theories (with ∀, ∃)

Theory Selection Guide:

• QF_LIA: Integer variables, linear constraints (x + 2*y <= 10)
• QF_LRA: Real-valued variables, linear constraints
• QF_BV: Fixed-width integers, bitwise operations
• Arrays: Index-value mappings, read/write operations
• QF_UF: Functions without interpretation (symbolic functions)

2. Z3 Architecture

User Code (Python)
    ↓
Z3 Python Bindings (z3-solver)
    ↓
Z3 Core Engine (C++)
    ├── Preprocessor (simplification)
    ├── Theory Solvers (LIA, BV, Arrays)
    ├── SAT Solver (CDCL core)
    └── Tactic Framework (strategies)
    ↓
Result: sat, unsat, unknown

3. Solver Modes

Standard Mode (check):

from z3 import *

s = Solver()
x = Int('x')
s.add(x > 0)
s.add(x < 10)
result = s.check()  # sat, unsat, unknown
if result == sat:
    print(s.model())  # Solution: x = 1 (or any value in [1, 9])

Optimization Mode (Optimize):

opt = Optimize()
x = Int('x')
y = Int('y')
opt.add(x + y <= 10)
opt.add(x >= 0, y >= 0)
opt.maximize(x + 2*y)  # Objective function
if opt.check() == sat:
    print(opt.model())  # x=0, y=10 (maximizes objective)

4. Constraint Types

Arithmetic Constraints:

x, y = Ints('x y')
constraints = [
    x + y == 10,           # Linear equality
    2*x - 3*y <= 5,        # Linear inequality
    x * y == 24,           # Nonlinear (switches to NRA theory)
    x % 2 == 0,            # Modulo (integer division)
]

Bitvector Constraints:

x = BitVec('x', 32)  # 32-bit bitvector
y = BitVec('y', 32)
constraints = [
    x & y == 0,              # Bitwise AND
    x | y == 0xFFFFFFFF,     # Bitwise OR (all bits set)
    x >> 2 == y,             # Logical right shift
    SignExt(16, x) == y,     # Sign extension
]

Array Constraints:

A = Array('A', IntSort(), IntSort())  # Array: Int -> Int
i, j = Ints('i j')
constraints = [
    Store(A, i, 10)[i] == 10,         # Write then read
    Select(A, i) == Select(A, j),     # Same values at i, j
]

Implementation Patterns

Pattern 1: Basic Constraint Solving

from z3 import *

# Problem: Find x, y such that x^2 + y^2 = 25 and x > y
def solve_pythagorean():
    s = Solver()
    x = Int('x')
    y = Int('y')

    s.add(x*x + y*y == 25)
    s.add(x > y)

    if s.check() == sat:
        m = s.model()
        print(f"Solution: x={m[x]}, y={m[y]}")
        # Output: x=5, y=0 or x=4, y=3 or x=3, y=-4, etc.
    else:
        print("No solution")

solve_pythagorean()

Pattern 2: Multiple Solutions with Blocking Clauses

def find_all_solutions(solver, variables, max_solutions=10):
    """Find multiple solutions by blocking previous ones"""
    solutions = []

    for _ in range(max_solutions):
        if solver.check() != sat:
            break

        m = solver.model()
        solution = {v: m[v] for v in variables}
        solutions.append(solution)

        # Block this solution
        block = Or([v != m[v] for v in variables])
        solver.add(block)

    return solutions

# Example: Find all x, y pairs where x + y = 5, 0 <= x,y <= 5
s = Solver()
x, y = Ints('x y')
s.add(x + y == 5)
s.add(x >= 0, x <= 5)
s.add(y >= 0, y <= 5)

solutions = find_all_solutions(s, [x, y])
for sol in solutions:
    print(f"x={sol[x]}, y={sol[y]}")
# Output: (0,5), (1,4), (2,3), (3,2), (4,1), (5,0)

Pattern 3: Optimization with Multiple Objectives

def solve_multiobjective():
    """Lexicographic optimization: prioritize objectives"""
    opt = Optimize()
    x, y = Ints('x y')

    # Constraints
    opt.add(x + y <= 10)
    opt.add(x >= 0, y >= 0)

    # Primary objective: maximize x
    h1 = opt.maximize(x)

    # Secondary objective: maximize y (given optimal x)
    h2 = opt.maximize(y)

    if opt.check() == sat:
        print(f"x={opt.model()[x]}, y={opt.model()[y]}")
        print(f"Objective 1: {opt.lower(h1)} <= x <= {opt.upper(h1)}")
        print(f"Objective 2: {opt.lower(h2)} <= y <= {opt.upper(h2)}")
    # Output: x=10, y=0 (maximizes x first, then y)

solve_multiobjective()

Pattern 4: Unsat Core Extraction

def analyze_conflicting_constraints():
    """Find minimal subset of constraints that cause unsat"""
    s = Solver()
    x = Int('x')

    # Create named constraints
    c1 = x > 10
    c2 = x < 5
    c3 = x >= 0
    c4 = x <= 100

    # Add with tracking
    s.assert_and_track(c1, 'c1')
    s.assert_and_track(c2, 'c2')
    s.assert_and_track(c3, 'c3')
    s.assert_and_track(c4, 'c4')

    if s.check() == unsat:
        core = s.unsat_core()
        print(f"Conflicting constraints: {core}")
        # Output: [c1, c2] (x > 10 and x < 5 conflict)

analyze_conflicting_constraints()

Pattern 5: Theory-Specific Tactics

def solve_with_tactics():
    """Use tactics for performance tuning"""
    x, y = Ints('x y')
    formula = And(x + y == 10, x - y == 2)

    # Strategy: simplify, then solve with LIA solver
    tactic = Then('simplify', 'qflia')  # Quantifier-free LIA
    solver = tactic.solver()
    solver.add(formula)

    if solver.check() == sat:
        print(solver.model())
    # Output: x=6, y=4

solve_with_tactics()

Pattern 6: Incremental Solving

def incremental_solving():
    """Efficient solving with push/pop for backtracking"""
    s = Solver()
    x, y = Ints('x y')

    # Base constraints
    s.add(x + y <= 10)

    # Try scenario 1: x > 5
    s.push()
    s.add(x > 5)
    if s.check() == sat:
        print(f"Scenario 1: {s.model()}")
    s.pop()

    # Try scenario 2: y > 5 (independent of scenario 1)
    s.push()
    s.add(y > 5)
    if s.check() == sat:
        print(f"Scenario 2: {s.model()}")
    s.pop()

incremental_solving()

Pattern 7: Array Reasoning

def verify_array_swap():
    """Verify swap operation using array theory"""
    A = Array('A', IntSort(), IntSort())
    i, j = Ints('i j')

    # Swap operation
    A_swap = Store(Store(A, i, Select(A, j)), j, Select(A, i))

    # Verify: after swap, A[i] == old_A[j] and A[j] == old_A[i]
    s = Solver()
    s.add(Select(A_swap, i) != Select(A, j))  # Should be unsat

    if s.check() == unsat:
        print("Swap verified correct")
    else:
        print(f"Bug found: {s.model()}")

verify_array_swap()

Pattern 8: Bitvector Reasoning

def check_overflow():
    """Detect integer overflow in bitvector arithmetic"""
    x = BitVec('x', 8)  # 8-bit unsigned integer
    y = BitVec('y', 8)

    s = Solver()
    s.add(x + y > 255)  # Overflow condition
    s.add(ULT(x + y, x))  # Result < x (overflow check)

    if s.check() == sat:
        m = s.model()
        print(f"Overflow: {m[x]} + {m[y]} = {m.evaluate(x + y)}")
        # Example: 200 + 100 = 44 (mod 256)

check_overflow()

Quick Reference

Installation

# Python Z3
pip install z3-solver

# Or with uv
uv add z3-solver

# Verify
python -c "import z3; print(z3.get_version_string())"

Common Types

# Integer variables
x = Int('x')
x, y, z = Ints('x y z')

# Real variables
r = Real('r')

# Boolean variables
b = Bool('b')

# Bitvectors
bv = BitVec('bv', 32)  # 32-bit

# Arrays
A = Array('A', IntSort(), IntSort())  # Int -> Int
B = Array('B', BitVecSort(32), IntSort())  # BitVec(32) -> Int

Constraint Operations

# Logical
And(c1, c2, c3)
Or(c1, c2)
Not(c)
Implies(c1, c2)
Xor(c1, c2)

# Arithmetic
x + y, x - y, x * y, x / y  # Division is integer division for Int
x % y  # Modulo
x ** 2  # Exponentiation (switches to nonlinear)

# Comparison
x == y, x != y
x < y, x <= y, x > y, x >= y

# Bitvector
x & y, x | y, x ^ y  # Bitwise AND, OR, XOR
~x  # Bitwise NOT
x << n, x >> n  # Shifts
ZeroExt(n, x), SignExt(n, x)  # Extension
Extract(high, low, x)  # Bit extraction

# Array
Select(A, i)  # Read A[i]
Store(A, i, v)  # Write A[i] = v

Solver API

s = Solver()
s.add(constraint)  # Add constraint
s.check()  # Returns sat, unsat, or unknown
s.model()  # Get model if sat
s.push()  # Save state
s.pop()  # Restore state
s.reset()  # Clear all constraints

# Optimization
opt = Optimize()
opt.add(constraint)
h = opt.maximize(expr)  # or minimize(expr)
opt.check()
opt.model()
opt.lower(h), opt.upper(h)  # Objective bounds

Tactics

# Common tactics
tactics = [
    'simplify',      # Algebraic simplification
    'solve-eqs',     # Gaussian elimination
    'qflia',         # Quantifier-free linear integer arithmetic
    'qfbv',          # Quantifier-free bitvectors
    'qfnra',         # Quantifier-free nonlinear real arithmetic
    'sat',           # SAT solver
    'smt',           # Full SMT solver
]

# Use tactic
tactic = Then('simplify', 'qflia')
solver = tactic.solver()

Performance Tips

# 1. Set timeout (milliseconds)
s = Solver()
s.set('timeout', 5000)  # 5 seconds

# 2. Enable parallel mode
set_param('parallel.enable', True)

# 3. Use appropriate theory
# QF_LIA faster than general arithmetic
# Use bitvectors for bounded integers

# 4. Simplify before solving
from z3 import simplify
formula = simplify(complex_formula)
s.add(formula)

# 5. Incremental solving with push/pop
s.push()
s.add(temporary_constraint)
s.check()
s.pop()

Anti-Patterns

Anti-Pattern 1: Over-Constraining

Problem: Adding redundant or conflicting constraints.

# BAD: Redundant constraints slow down solver
s = Solver()
x = Int('x')
s.add(x > 0)
s.add(x > 1)  # Implies x > 0 (redundant)
s.add(x >= 2)  # Also redundant

Solution: Simplify constraints first.

# GOOD: Minimal constraint set
s = Solver()
x = Int('x')
s.add(x >= 2)  # Sufficient (implies x > 0 and x > 1)

Anti-Pattern 2: Wrong Theory Selection

Problem: Using nonlinear arithmetic when linear suffices.

# BAD: Nonlinear (slower)
x, y = Reals('x y')
s = Solver()
s.add(x * y == 10)  # Nonlinear

Solution: Reformulate as linear when possible.

# GOOD: Linear (if y is constant)
x = Real('x')
y_value = 2.0
s = Solver()
s.add(x == 10 / y_value)  # Linear

Anti-Pattern 3: Ignoring Solver Status

Problem: Accessing model without checking satisfiability.

# BAD: May crash if unsat
s = Solver()
s.add(False)
m = s.model()  # Error: solver is unsat

Solution: Always check status first.

# GOOD: Check before model access
if s.check() == sat:
    m = s.model()
else:
    print("No solution exists")

Anti-Pattern 4: Inefficient Blocking Clauses

Problem: Expensive enumeration of solutions.

# BAD: Blocks each variable separately (exponential clauses)
for _ in range(100):
    if s.check() == sat:
        m = s.model()
        for v in variables:
            s.add(v != m[v])  # Wrong: adds 1 clause per variable

Solution: Block entire solution at once.

# GOOD: Single blocking clause per solution
for _ in range(100):
    if s.check() == sat:
        m = s.model()
        s.add(Or([v != m[v] for v in variables]))  # 1 clause

Anti-Pattern 5: Not Using Push/Pop

Problem: Recreating solver for each scenario.

# BAD: Recreates solver (slow)
for scenario in scenarios:
    s = Solver()  # New solver each time
    s.add(base_constraints)
    s.add(scenario)
    s.check()

Solution: Use incremental solving.

# GOOD: Reuse solver with push/pop
s = Solver()
s.add(base_constraints)
for scenario in scenarios:
    s.push()
    s.add(scenario)
    s.check()
    s.pop()

Real-World Applications

Application 1: Sudoku Solver

def solve_sudoku(grid):
    """Solve 9x9 Sudoku using Z3"""
    cells = [[Int(f"c_{i}_{j}") for j in range(9)] for i in range(9)]

    s = Solver()

    # Each cell in [1, 9]
    for i in range(9):
        for j in range(9):
            s.add(And(cells[i][j] >= 1, cells[i][j] <= 9))

    # Row constraints
    for i in range(9):
        s.add(Distinct([cells[i][j] for j in range(9)]))

    # Column constraints
    for j in range(9):
        s.add(Distinct([cells[i][j] for i in range(9)]))

    # 3x3 box constraints
    for box_i in range(3):
        for box_j in range(3):
            box = [cells[i][j]
                   for i in range(box_i*3, box_i*3+3)
                   for j in range(box_j*3, box_j*3+3)]
            s.add(Distinct(box))

    # Add initial grid values
    for i in range(9):
        for j in range(9):
            if grid[i][j] != 0:
                s.add(cells[i][j] == grid[i][j])

    if s.check() == sat:
        m = s.model()
        return [[m.evaluate(cells[i][j]).as_long() for j in range(9)]
                for i in range(9)]
    return None

Application 2: Program Verification

def verify_binary_search(arr_size=10):
    """Verify binary search finds element if present"""
    A = Array('A', IntSort(), IntSort())
    target = Int('target')
    low, high, mid = Ints('low high mid')

    s = Solver()

    # Array is sorted
    for i in range(arr_size - 1):
        s.add(Select(A, i) <= Select(A, i+1))

    # Target exists at some index
    exists_idx = Int('exists_idx')
    s.add(And(exists_idx >= 0, exists_idx < arr_size))
    s.add(Select(A, exists_idx) == target)

    # Binary search logic (simplified)
    s.add(low == 0)
    s.add(high == arr_size - 1)
    s.add(mid == (low + high) / 2)

    # After one iteration, mid should narrow search
    found = Select(A, mid) == target
    go_left = Select(A, mid) > target
    go_right = Select(A, mid) < target

    # Check: we always make progress
    s.add(Not(Or(found, And(go_left, exists_idx < mid),
                       And(go_right, exists_idx > mid))))

    if s.check() == unsat:
        print("Binary search verified: always makes progress")
    else:
        print(f"Bug found: {s.model()}")

verify_binary_search()

Related Skills

• sat-solving-strategies.md: Pure Boolean SAT solving, CDCL algorithms
• smt-theory-applications.md: Advanced SMT applications, theory combinations
• constraint-propagation.md: CSP techniques, arc consistency
• lean-theorem-proving.md: Interactive theorem proving
• program-analysis.md: Static analysis, abstract interpretation

References

• Z3 Tutorial: https://ericpony.github.io/z3py-tutorial/guide-examples.htm
• Z3 API Docs: https://z3prover.github.io/api/html/namespacez3py.html
• SMT-LIB Standard: http://smtlib.cs.uiowa.edu/
• Book: "Decision Procedures" by Kroening & Strichman

Troubleshooting

Problem: Solver returns "unknown"

• Cause: Nonlinear constraints, quantifiers, or timeout
• Fix: Simplify formula, increase timeout, or use approximations

Problem: Slow solving

• Cause: Wrong theory, over-constraining, or poor variable ordering
• Fix: Use tactics, simplify constraints, or enable parallel mode

Problem: Unexpected model values

• Cause: Under-constrained problem (multiple solutions)
• Fix: Add more constraints or enumerate all solutions

Problem: ImportError for z3

• Cause: Not installed or wrong environment
• Fix: pip install z3-solver or uv add z3-solver