SMT Solvers

Boolean Satisfiability (SAT)

The SAT Problem

Given a Boolean formula in conjunctive normal form (CNF) — a conjunction of clauses, each a disjunction of literals — determine whether there exists a satisfying assignment. SAT is NP-complete (Cook-Levin theorem, 1971), yet modern solvers handle industrial instances with millions of variables and clauses, a phenomenon driven by structural regularity in real-world formulas.

DPLL Algorithm

The Davis-Putnam-Logemann-Loveland (DPLL, 1962) algorithm is the foundation of all modern SAT solvers:

Unit propagation (BCP): If a clause has one unassigned literal, that literal must be true. Propagate transitively — this is the main driver of deduction, consuming 80-90% of solver runtime.
Pure literal elimination: If a variable appears with only one polarity, assign it to satisfy those clauses.
Decision: Choose an unassigned variable and assign a value (branching).
Backtracking: If a conflict (empty clause) is reached, undo the last decision and try the opposite value.

DPLL performs chronological backtracking — it undoes decisions in reverse order. This can be inefficient: the conflict may be caused by a much earlier decision.

CDCL (Conflict-Driven Clause Learning)

CDCL (Marques-Silva and Sakallah, 1996; Moskewicz et al., 2001) extends DPLL with:

Conflict analysis: When a conflict occurs, analyze the implication graph to identify the root cause — a subset of decisions sufficient to cause the conflict. Learn a new clause (the conflict clause) that prevents the same combination of assignments in the future.

Non-chronological backtracking (backjumping): Instead of undoing just the last decision, jump back to the decision level identified by conflict analysis. The 1-UIP (Unit Implication Point) scheme identifies the most recent decision level responsible: the conflict clause has exactly one literal at the backtrack level.

Restarts: Periodically restart the search from scratch, retaining learned clauses. Prevents getting trapped in unproductive search regions. Modern strategies (Luby, geometric, glucose-based) tune restart frequency dynamically.

Clause database management: Learned clauses accumulate rapidly. Periodically delete low-quality clauses based on heuristics like LBD (Literal Block Distance) — the number of distinct decision levels in the clause. Low LBD clauses are "glue" that connects distant parts of the search and should be retained.

VSIDS (Variable State Independent Decaying Sum)

The decision heuristic is critical to CDCL performance. VSIDS (Moskewicz et al., 2001):

Each variable has an activity score, incremented when the variable appears in a conflict clause.
All scores decay periodically (multiply by a factor < 1).
Branch on the most active unassigned variable.

This focuses the search on variables involved in recent conflicts — the "hot" region of the formula. VSIDS-family heuristics (EVSIDS, CHB, LRB) are used by virtually all competitive SAT solvers.

Watched Literals

Efficient unit propagation via the two-watched-literal scheme: For each clause, watch two unassigned literals. Only when a watched literal is falsified does the solver inspect the clause. This avoids iterating over all clauses at each propagation step — critical for performance on large instances.

Modern SAT Solvers

MiniSat (Eén and Sörensson, 2003): Clean reference implementation of CDCL. Foundation for many derivative solvers. CaDiCaL (Biere, 2017): State-of-the-art solver with advanced inprocessing (variable elimination, subsumption, blocked clause elimination). Kissat: Biere's latest solver, winner of multiple SAT competitions.

Satisfiability Modulo Theories (SMT)

From SAT to SMT

SMT extends SAT by replacing Boolean atoms with predicates from background theories. Instead of asking "is φ satisfiable?" for Boolean φ, SMT asks "is φ satisfiable in theory T?" where atoms are theory predicates.

Example: (x + 2 > y) ∧ (y > x + 3) is a conjunction of linear arithmetic atoms. Boolean satisfiable (assign both true), but unsatisfiable in the theory of linear arithmetic.

The DPLL(T) Architecture

The dominant SMT architecture combines a SAT solver with theory solvers:

Boolean abstraction: Replace each theory atom with a fresh Boolean variable. Feed the Boolean skeleton to CDCL.
Theory checking: When CDCL finds a satisfying Boolean assignment, the theory solver checks if the corresponding theory atoms are jointly satisfiable.
Theory propagation: The theory solver deduces implied theory atoms (e.g., from x < 5, deduce x < 10) and feeds them back to CDCL as unit clauses.
Theory conflict clauses: If the theory solver detects unsatisfiability, it generates a theory conflict clause (explaining the contradiction) and adds it to CDCL for learning and backjumping.

Incremental theory solving: The theory solver operates incrementally as CDCL makes/undoes assignments. It maintains a stack of asserted atoms and checks consistency after each push.

Key Theories

Equality and Uninterpreted Functions (EUF)

Atoms: f(a,b) = g(c), a ≠ b. Theory of equality with function congruence: if a = c and b = d then f(a,b) = f(c,d). Solved by union-find with congruence closure. O(n log n) time. Foundation for reasoning about data structures, function calls, and type hierarchies.

Linear Integer Arithmetic (LIA) / Linear Real Arithmetic (LRA)

Atoms: linear inequalities Σ aᵢxᵢ ≤ c. LRA is decidable via the Simplex method (adapted for incrementality and backtracking — Dutertre and de Moura, 2006). LIA extends LRA with integrality constraints, solved by branch-and-bound or Omega test. LRA is in polynomial time; LIA is NP-complete.

Difference logic: Special case where all atoms have the form xᵢ - xⱼ ≤ c. Solvable in polynomial time via Bellman-Ford shortest paths. Used in scheduling and timing verification.

Bit-Vectors (BV)

Fixed-width integers with wrap-around arithmetic, bit operations (and, or, xor, shift), extraction, concatenation. Models machine arithmetic precisely. Solved by bit-blasting: translate to SAT by expanding each bit-vector variable into Boolean variables. For 32-bit vectors, each variable becomes 32 Boolean variables. Effective but formula size scales linearly with bit-width.

Word-level reasoning: Avoid bit-blasting by reasoning at the word level. Algebraic simplifications, abstraction-refinement, and interval-based reasoning can solve many BV queries without full expansion.

Arrays

Theory of arrays with select (read) and store (write): select(store(a, i, v), j) = ite(i = j, v, select(a, j)). Extended with extensionality: two arrays are equal iff they agree on all indices. Used for modeling memory, buffers, and data structures.

Strings and Regular Expressions

Theory of string operations: concatenation, length, substring, contains, indexOf, replace. Regular expression membership: str ∈ regex. Highly relevant for analyzing web applications (input validation, SQL injection). Decidability is theory-dependent; most practical fragments are decidable but expensive.

CVC5 string solver: Uses a combination of word equations theory (Makanin's algorithm descendants) and length reasoning. Z3 uses an algebraic approach with sequence axioms.

Theory Combination

Nelson-Oppen Framework

When a formula involves atoms from multiple theories (e.g., linear arithmetic and uninterpreted functions), the Nelson-Oppen method (1979) combines theory solvers:

Purification: Separate the formula into theory-pure components by introducing fresh variables at theory boundaries. E.g., f(x+1) > x becomes f(y) > x ∧ y = x + 1 with y fresh.
Equality propagation: Theory solvers exchange equalities (and disequalities) between shared variables. If the arithmetic solver deduces y = z, it informs the EUF solver. Iterate until fixed point or contradiction.

Requirements: Theories must be stably infinite (every satisfiable formula has an infinite model) and have disjoint signatures (no shared function/predicate symbols). Most standard theories satisfy these.

Convexity: A theory is convex if whenever it implies a disjunction of equalities, it implies one of the disjuncts. Convex theories (LRA, EUF) require only equality propagation. Non-convex theories (LIA, BV) require case-splitting on disjunctions.

Model-Based Theory Combination

Alternative to Nelson-Oppen: the leading theory solver produces a model (concrete assignment), and other solvers check consistency with this model. If inconsistent, they produce a theory lemma. Avoids explicit equality propagation. Used in Z3's approach.

Solvers

Z3 (Microsoft Research)

The most widely used SMT solver. Features:

Efficient DPLL(T) engine with advanced theory solvers
E-matching for quantifier instantiation (heuristic for ∀-quantified formulas)
Model-based quantifier instantiation (MBQI): Find candidate instances by examining the current model
Specialized tactics: simplification, bit-blasting, Horn clause solving (Spacer/μZ)
Rich API (Python, C, C++, Java, .NET, OCaml, Rust)
Used in Dafny, Boogie, F*, KLEE, Crucible, and hundreds of verification tools

CVC5

Stanford/University of Iowa solver. Successor to CVC4. Notable for:

Strong string solver
SyGuS (syntax-guided synthesis) support
Finite model finding for quantified formulas
Proof production (machine-checkable proofs of unsatisfiability)
Competitive with Z3 on most benchmarks

Other Solvers

Yices 2: Efficient for linear arithmetic and bit-vectors. Lightweight and fast.
Boolector/Bitwuzla: Specialized for bit-vectors and arrays. Top performers on QF_BV benchmarks.
MathSAT 5: Strong on interpolation (useful for CEGAR-based verification).

Applications

Program Verification

SMT solvers are the backend for deductive verification tools. Verification conditions (VCs) generated from annotated programs are discharged by SMT queries. Dafny, Why3, and KeY translate program correctness proofs to SMT.

Symbolic Execution

Every path condition check is an SMT query. Solver performance directly determines symbolic execution throughput. Incremental solving (push/pop) exploits the fact that consecutive queries share most constraints.

Model Checking

Bounded model checking (BMC) unrolls a transition system k times and checks if a property violation is reachable. The resulting formula (initial state ∧ transition^k ∧ ¬property) is an SMT query. IC3/PDR uses SMT for inductive generalization of reachable states.

Constraint Solving in Synthesis

Program synthesis generates programs meeting a specification. SyGuS formulates synthesis as: find a program P such that ∀x. φ(x, P(x)). The CEGIS (Counterexample-Guided Inductive Synthesis) loop uses SMT to check candidates and generate counterexamples.

Test Generation

Solve path conditions to generate test inputs achieving specific coverage targets. Pex (IntelliTest in Visual Studio) uses Z3 to generate unit tests automatically.

Performance Considerations

Incremental Solving

Push/pop interface: add constraints incrementally, check satisfiability, then pop to remove constraints. Essential for symbolic execution (path conditions grow along paths) and CEGAR (incrementally refined abstractions). Much faster than solving from scratch each time.

Quantifier Handling

Quantified SMT (∀, ∃) is undecidable in general. Practical approaches:

E-matching: Instantiate universally quantified axioms by matching patterns (triggers) against ground terms. Sound for refutation but incomplete.
MBQI: Use the current model to guide instantiation. Complete for some decidable fragments.
Finite model finding: Search for small models. Complete for formulas with finite domain quantification.

Optimization (MaxSMT, Optimization Modulo Theories)

Extend SMT to optimize an objective function subject to theory constraints. MaxSMT: maximize the number of satisfied soft clauses. OMT: minimize a theory term (e.g., minimize x subject to constraints). Z3's Optimize module and OptiMathSAT support these.