Z3 solver note

posted
read
182 words · 1 min
tags
#z3#smt#constraints#ctf
contents

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
  • Outdoor classes cannot happen after 12
  • 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:

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

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