SMT Solving and Z3

SMT Solving and Z3#

Idea#

SMT, satisfiability modulo theories, extends propositional satisfiability (SAT) by adding interpreted functions and predicates from various decidable first-order theories. For example, instead of just Boolean variables, we can have:

  • Linear arithmetic: variables like x, y with constraints x + y > 10, 2x - 3y ≤ 5

  • Bit-vectors: variables like a, b with bitwise operations a & b = 0xFF, a << 2 = b

  • Arrays: array variables A, B with operations A[i] = B[j], store(A, i, v)

  • Uninterpreted functions: function symbols f, g with constraints f(x) = g(y), f(f(x)) = x

Remark: This looks very similar to constraint programming. So what is the difference? MiniZinc can call Z3 as a backend and SMT-solvers are used in CP competitions. The answer to the question may well be how different communities in computer science research evolved historically. We should add a section that explores this history.

Basic Theory#

First-order logic is not decidable, but it does contain some decidable theories. SMT leverages special solvers for decidable first-order theories. Moreover, under certain conditions different decidable theories can be combined into larger ones.

Decidable First-Order Theories#

Typically, decidability requires that the formulas have to by quantifier-free (QF) but there are exceptions, most famously the theory of real closed fields.

Real Closed Fields (RCF) have a decidable theory due to Tarski’s quantifier elimination (1930s) which shows that any first-order formula over reals can be reduced to a quantifier-free formula:

  • Variables: Real numbers

  • Operations: +, -, *, /, <, ≤, >, ≥, =, quantifiers ∀, ∃

  • Example: ∀x∀y. x² + y² = 1 → x > 0 ∨ x < 0 (every point on unit circle is not zero)

Linear Arithmetic (QFLRA/QFLIA) can be solved using simplex algorithm or Fourier-Motzkin elimination:

  • Variables: Rationals (QFLRA) or Integers (QFLIA)

  • Operations: +, -, <, ≤, >, ≥, =

  • Example: x + 2y ≤ 10 ∧ x > 0

Equality with Uninterpreted Functions (EUF) can be solved with the congruence closure algorithm (1970s):

  • Variables: Any domain, with function symbols f, g, etc.

  • Operations: Function application, equality

  • Example: f(x) = g(y) ∧ f(f(x)) = x

Arrays (QF_A) can be reduced to EUF + axioms

  • Variables: Arrays A, B, indices i, j, values v

  • Operations: select(A, i), store(A, i, v)

  • Example: select(store(A, i, v), j) = select(A, j) ∧ i ≠ j

Bit-vectors (QF_BV) can be reduced to SAT or solved with specialized algorithms:

  • Variables: Fixed-width integers (e.g., 32-bit)

  • Operations: Bitwise (&, |, ^, ~), arithmetic (+, *), shifts (<<, >>)

  • Example: x & y = 0 ∧ x | y = 0xFF

Difference Logic (QF_IDL/QF_RDL) can be solved using shortest path algorithms

  • Variables: Integers or Reals

  • Operations: Differences x - y ≤ c, equality x = y

  • Example: x - y ≤ 5 ∧ y - z ≤ 3 ∧ z - x ≤ -10

Theory Combination: The Nelson-Oppen Method#

See Martin’s Lecture Notes on SMT Solving: Nelson-Oppen.

Z3#

Z3 Tutorial

There are different ways to use Z3. We start with the playground and then learn how to call Z3 from Python.

Z3 Playground#

Array bounds#

Read the following program written in SMT-LIB. For background, I recommend to read Chapter 2 as well as pages 22, 55-56, 76 of the SMT-LIB Standard.

(declare-const i Int)
(declare-const array_size Int)

; Set values
(assert (= array_size 10))
(assert (= i 15))

; Check if bounds can be violated
(assert (not (and (<= 0 i) (< i array_size))))

(check-sat)
(get-model)

Paste the code into the Z3 Playground. How do you interpret the result?

Answer the question by keep changing the code and predicting the results you expect.

Guessing a number#

Here’s a more interesting example where we let Z3 find values for variables:

(declare-const x Int)
(declare-const y Int)

(assert (= (+ x y) 15))
(assert (= (- x y) 5))

(check-sat)
(get-model)

Exercise: Create your own “guessing the number” puzzle.

More Solvers#

SMT-LIB is a standardized language used by many SMT solvers, not just Z3. Try the programs above with:

Other SMT-solvers that accept SMT-LIB are:

Z3 in Python#

Interactive Z3 examples are available below via Colab or Binder or download a copy here.

Try it interactively:

Open In Colab 🚀 Google Colab (Recommended - Fast & Reliable)

Binder 🐳 Binder (Alternative)

Practical Examples:

i) Prove that array access is always within bounds in a loop:

(declare-fun i () Int)
(declare-fun n () Int)
(assert (and (>= i 0) (< i n)))   ; loop invariant
(assert (not (< i n)))            ; try to violate it
(check-sat)

Explanation: Z3 can prove safety properties like “no out-of-bounds access occurs”. This connects to static analysis and model checking.

References#

Contents