Z3 solver note

Posted on In , Views: Disqus: Word count in article: 301 Reading time ≈ 1 mins.

Z3 is an SMT solver. You describe a problem as variables plus constraints, and Z3 finds assignments that satisfy them (or proves none exist).

  • SMT = "Satisfiability Modulo Theories"
  • Think of it as: "declare rules first, solve later"
  • Usually not a replacement for a hand-tuned algorithm, but great when rules change often

Typical use cases

  • Scheduling and timetabling
  • Resource allocation
  • Program analysis and verification
  • Reverse engineering and CTF constraints

Example scheduling constraints:

  • Mary cannot work Tuesdays
  • John cannot teach before 10:00
  • Outdoor classes cannot happen after 12:00
  • Susan and Sarah cannot teach the same class

This is exactly the kind of constraint-heavy problem where solvers shine.

Core variable types

  • Int(name): integer (no fractions)
  • Real(name): real/rational number
  • Bool(name): boolean (True / False)
  • BitVec(name, bits): fixed-width integer with wraparound (useful for low-level/crypto work)

You can declare multiple variables at once with plural helpers, for example:

1
a, b, c, d, e = Bools("a b c d e")

Common operators and helpers

  • And(*args): all conditions must hold
  • Or(*args): at least one condition must hold
  • Not(x): logical negation
  • Xor(a, b): exactly one is true
  • Distinct(*args): all expressions have different values
  • LShR(n, b): logical right shift (fills with 0)

Notes:

  • Arithmetic: +, -, *, /, **
  • Bitwise: <<, >>, &, |
  • Comparisons: ==, !=, <, >, <=, >=
  • For bit-vectors, >> is arithmetic shift; use LShR for logical shift

Example

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
from z3 import Real, Solver, sat

s = Solver()

x = Real("x")
y = Real("y")
z = Real("z")

s.add(x * x + y == 16)
s.add(z**3 == 27)
s.add(x * z == 6)

if s.check() == sat:
    m = s.model()
    print("model:", m)
    print("x =", m.eval(x))
    print("y =", m.eval(y))
    print("z =", m.eval(z))
else:
    print("unsat")

References

  • https://asibahi.github.io/thoughts/a-gentle-introduction-to-z3/
  • https://www.hillelwayne.com/post/z3-examples/
  • https://book.jorianwoltjer.com/cryptography/custom-ciphers/z3-solver