Nelson–Oppen combination

A method for deciding satisfiability of quantifier-free formulas in a union of theories $T_1\cup T_2$, given a decision procedure for each. The formula is split into pure parts, one per theory, and the procedures exchange equalities between shared variables until one finds a contradiction or neither can add anything.

The conditions: the signatures of $T_1$ and $T_2$ share nothing but equality, and both theories are stably infinite, meaning every quantifier-free formula satisfiable in the theory has an infinite model. Linear arithmetic over $\mathbb{Q}$ and the theory of uninterpreted functions both qualify.

First, purification replaces every subterm that mixes the two signatures by a fresh variable, until each literal belongs to one theory. With linear real arithmetic and uninterpreted functions:

becomes, with $u,v$ fresh,

The shared variables are $x,y,u,v$. Each procedure checks its part and reports the equalities between shared variables that its part implies:

arithmetic   x <= y and y <= x          implies  x = y     -> functions
functions    x = y, congruence          implies  u = v     -> arithmetic
arithmetic   u - v != 0 and u = v       unsatisfiable

A theory is convex when a conjunction of its literals that implies a disjunction of equalities between variables implies one of them. For convex theories the exchange above is complete. Linear arithmetic over $\mathbb{Q}$ is convex; over $\mathbb{Z}$ it is not:

Together with $f(x)\ne f(1)\wedge f(x)\ne f(2)$ the formula is unsatisfiable, yet no single equality is ever implied, so the exchange has nothing to send. Non-convex theories need case splitting: the procedure guesses an arrangement, a partition of the shared variables into equivalence classes, and the formula is satisfiable exactly when some arrangement is consistent with both pure parts. SMT solvers let the SAT layer do that guessing, by branching on the equalities between shared variables as if they were atoms.

Stable infiniteness is what makes the arrangement sufficient. Each part's model can be taken infinite and of the same cardinality, and then the two agree on which shared variables are equal, so they can be glued into one model of the union.

• Congruence closureThe decision procedure for equality over uninterpreted functions: union-find plus the rule that equal arguments give equal applications. Merging two classes can therefore force their parents to merge, so the closure is computed by re-examining parents until nothing changes.
• DPLL(T)The standard architecture for an SMT solver: a CDCL core treats each theory atom as a boolean variable and searches as usual, while a theory solver checks each candidate assignment for theory consistency and hands back an explanation when it fails. The explanation becomes a learned clause, so the boolean search is what drives progress.
• SMTSatisfiability 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.
• Theory solverThe decision procedure plugged into a DPLL(T) core for one specific theory. Its interface is small: accept assertions, report consistent or inconsistent, and on inconsistency return a subset of the assertions that already conflict, because a smaller explanation becomes a stronger learned clause.

1. [1]G. Nelson, D. C. Oppen, “Simplification by cooperating decision procedures”, ACM TOPLAS 1 (1979).
2. [2]D. C. Oppen, “Complexity, convexity and combinations of theories”, Theoretical Computer Science 12 (1980).
3. [3]C. Tinelli, M. Harandi, “A new correctness proof of the Nelson–Oppen combination procedure”, FroCoS (1996).