SMT

also: satisfiability modulo theories, z3

Satisfiability modulo theories: SAT where the atoms are not opaque booleans but statements in some theory, such as linear arithmetic or equality over uninterpreted functions. The formula must be satisfiable both propositionally and in the theory, which is what makes SMT the engine under most program verifiers.

SAT where the atoms are no longer opaque. Instead of a boolean variable, an atom is a statement in some theory, and the formula must be satisfiable both propositionally and in that theory:

The theories that matter in practice are equality with uninterpreted functions, linear arithmetic over integers and reals, bit-vectors, and arrays. A propositional assignment that satisfies the boolean skeleton can still be rejected by the theory, and vice versa, which is exactly why the two have to be solved together rather than in sequence.

SMT is the engine under most program verification: a verification condition is a formula in these theories, and discharging it is a query. It is also what makes refinement types practical, since the subtyping obligations they generate are themselves such queries.

DPLL(T) · Theory solver · Refinement type

Congruence closure · Difference logic

• Implementing SAT in OCaml Part 3From SAT to SMT: the DPLL(T) architecture, reusing conflict-driven learning for theory conflicts, and a union-find equality theory.