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
⊨_T	—	T-satisfiable	Satisfiable in T
¬, ∧, ∨	—	Boolean	Propositional
=	—	Equality	In theory
read, write	—	Array	Select, store
+ , ≤	—	Arithmetic	Linear ops
bvadd, bvand	—	Bit-vector	BV operations

Metatheory. QF_LRA decidable (polynomial). QF_LIA decidable (NP-complete). QF_BV decidable (NP-complete). Array theory decidable for quantifier-free. Combination: if T₁, T₂ decidable and compatible, T₁ ∪ T₂ decidable. Quantified theories 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. Performance varies by problem structure. Quantifiers cause incompleteness/divergence. Non-linear arithmetic limited (undecidable in general). Model generation may be large. Theory combination has restrictions. Tuning solver options requires expertise.