Satisfiability Modulo Theories
Origin. SMT emerged from combining SAT solvers with decision procedures (2000s). Extends propositional satisfiability to first-order theories. Nelson-Oppen combination (1979). DPLL(T) architecture (Nieuwenhuis et al., 2006). Tools: Z3, CVC, Yices. Workhorse of modern verification.
Models. SAT solving with theory reasoning. SAT: is propositional formula satisfiable? SMT: is formula satisfiable in a theory? Theories: arithmetic, arrays, bit-vectors, strings. Combines efficient Boolean reasoning with theory-specific procedures. Practical decidability for useful fragments.
Formalism.
SMT problem: Given formula φ in theory T, is φ T-satisfiable?
Theories:
- QF_LIA: quantifier-free linear integer arithmetic
- QF_LRA: quantifier-free linear real arithmetic
- QF_BV: quantifier-free bit-vectors
- QF_A: quantifier-free arrays (read/write)
- QF_UF: quantifier-free uninterpreted functions
DPLL(T) architecture:
- SAT solver proposes Boolean assignment
- Theory solver checks consistency
- If conflict, theory explains (theory lemma)
- SAT solver backtracks using lemma
- Repeat until SAT or UNSAT
Theory combination (Nelson-Oppen): Combine theories T₁, T₂ if:
- Signatures disjoint (share only =)
- Both stably infinite
- Exchange equalities on shared variables
Example: (x + 2 = y) ∧ (read(write(a, x, 3), y - 2) = 3) Combines linear arithmetic and array theory.
Quantifiers: E-matching: instantiate ∀ with relevant terms. MBQI: model-based quantifier instantiation. Generally undecidable with quantifiers.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ⊨ | U+22A8 | True / Entailment | Written ⊨_T for satisfaction in the theory T |
| T | U+0054 | Latin capital T / Theory | The background theory constraining the symbols |
| φ | U+03C6 | Phi / Formula | The input whose T-satisfiability is asked |
| ¬ | U+00AC | Not sign | Propositional negation |
| ∧ | U+2227 | Logical and | Propositional conjunction |
| ∨ | U+2228 | Logical or | Propositional disjunction |
| ∀ | U+2200 | For all | Quantifier handled by E-matching or MBQI |
| = | U+003D | Equals sign | The predicate shared by all combined theories |
| ≤ | U+2264 | Less-than or equal to | Arithmetic literal |
| + | U+002B | Plus sign | Arithmetic operation |
| read, write | — | Array operations | Select and store |
| bvadd, bvand | — | Bit-vector operations | Modular addition, bitwise conjunction |
| QF_ | — | Fragment prefix | Marks a quantifier-free SMT-LIB logic |
| DPLL(T) | — | Solver architecture | SAT search coupled to a theory solver |
Metatheory. The standard quantifier-free fragments are all NP-complete, none of them polynomial: QF_LRA, QF_LIA, QF_UF, and QF_A alike. The polynomial procedures — simplex for linear real arithmetic, congruence closure for uninterpreted functions — decide conjunctions of literals; arbitrary Boolean structure over those literals restores NP-hardness, and DPLL(T) exists precisely to manage that structure. QF_BV is NP-complete when bit-widths are written in unary and NEXPTIME-complete when they are written in binary (Kovásznai, Fröhlich, Biere), which is why bit-blasting scales the way it does. Combination: under the Nelson-Oppen conditions above — disjoint signatures and stable infiniteness — decidability of T₁ and T₂ gives decidability of T₁ ∪ T₂. Quantified theories are often undecidable.
Applies to. Software verification (Dafny, F*, Why3). Hardware verification (bit-vectors). Symbolic execution. Test generation. Constraint solving. Type checking (refinement types). Security analysis. Compiler optimization verification.
Limitations. Decidability holds for the quantifier-free fragments and stops there: full first-order validity is undecidable by Church and Turing (1936), so a quantified query is answered by instantiation heuristics — E-matching depends on the trigger patterns attached to an axiom, and a query can therefore be answered "unknown" or diverge, with neither outcome carrying information about the formula. Nonlinear integer arithmetic is undecidable outright, by Matiyasevich's 1970 solution of Hilbert's tenth problem; the real closed field is decidable by Tarski, but with doubly exponential lower bounds for quantifier elimination (Davenport and Heintz, 1988). Combination is restricted by the Nelson-Oppen hypotheses — disjoint signatures and stable infiniteness — and theories that violate them, notably ones with only finite models, need separate treatment. Even the well-behaved fragments are NP-complete, so worst-case behaviour is exponential and the useful cases are exactly those where the structure is benign.
© 2026 Lingenic LLC