Nelson–Oppen Combination

Origin. Greg Nelson and Derek Oppen, "Simplification by cooperating decision procedures" (ACM TOPLAS 1, 1979). Robert Shostak's alternative method (1984) covered a narrower class more efficiently and its original correctness proof was wrong — Rueß and Shankar (2001) gave the first correct version, and Shostak's method is now understood as an instance of Nelson–Oppen. Tinelli and Harandi (1996) gave the clean model-theoretic proof; Ghilardi (2004) extended the result to non-disjoint signatures under model-completeness conditions.

Models. A combination theorem for theories, not logics — and the most heavily used result in this subdivision by a wide margin, since every SMT solver is an implementation of it. Two theories with disjoint signatures, each with a decidable quantifier-free satisfiability problem, are combined by taking the union of their axioms. The theorem says the union is decidable too, and the procedure says how: the two solvers exchange nothing but equalities between shared variables. Neither ever sees the other's symbols.

Formalism.

Setting: theories T₁, T₂ in signatures Σ₁, Σ₂ with Σ₁ ∩ Σ₂ = ∅ (except equality).

Stable infiniteness: Tᵢ is stably infinite if every Tᵢ-satisfiable quantifier-free formula is satisfiable in some model of Tᵢ with an infinite domain.

The theorem (Nelson–Oppen 1979; Tinelli–Harandi 1996): If T₁ and T₂ have disjoint signatures, are both stably infinite, and each has decidable quantifier-free satisfiability, then T₁ ∪ T₂ has decidable quantifier-free satisfiability.

The procedure:

1. Purify. Rewrite the input φ into φ₁ ∧ φ₂ with φᵢ over Σᵢ alone, introducing fresh variables for alien subterms. f(g(x)) = y with f ∈ Σ₁, g ∈ Σ₂ becomes f(v) = y ∧ v = g(x).
2. Share. Let V be the variables occurring in both φ₁ and φ₂.
3. Exchange. Each solver reports the equalities and disjunctions of equalities over V that its part entails; the other assumes them. Iterate to fixpoint.
4. Decide. φ is unsatisfiable iff some solver reports unsatisfiable.

Only equalities cross the boundary. Nothing else is shared, and nothing else needs to be.

Why it works: the shared language is just equality, so an arrangement of V — a partition saying which shared variables are equal — is all either theory can observe of the other. If both theories are satisfiable under the same arrangement, stable infiniteness supplies models of equal (infinite) cardinality, and a Löwenheim–Skolem argument fuses them into a model of the union. Stable infiniteness is exactly what guarantees the cardinalities can be made to agree; drop it and the fusion fails.

Convexity: Tᵢ is convex if whenever a conjunction of literals entails a disjunction of equalities, it entails one of the disjuncts. For convex theories, only single equalities need be exchanged, and step 3 runs in polynomial overhead. Non-convex theories — integer arithmetic, arrays, bitvectors — force case-splitting over arrangements, and the procedure becomes NP-hard in the number of shared variables. Linear rational arithmetic and equality with uninterpreted functions are convex; linear integer arithmetic is not: x ≥ 1 ∧ x ≤ 2 entails x = 1 ∨ x = 2 and neither disjunct.

Where the hypotheses bite: Disjointness is essential — two theories sharing a symbol can each constrain it, and the shared-equality interface does not see the conflict. Stable infiniteness is essential — a theory with only finite models can force a cardinality the other cannot match. Both have been relaxed: Ghilardi's non-disjoint combination via model-completeness and T₀-compatibility; polite and shiny theories (Ranise, Ringeissen, Zarba; Jovanović, Barrett) replace stable infiniteness with a witness-generation condition and admit theories with finite models.

Shostak's method: for theories that are canonizable and solvable, a congruence-closure-based procedure with better constants. The original proof was incorrect; the corrected accounts (Rueß–Shankar; Barrett, Dill, Stump) present it as an optimization of Nelson–Oppen rather than an alternative to it.

Symbols.

Metatheory. Nelson–Oppen is the transfer theorem that pays. Every other result in this subdivision is a statement about what a construction preserves; this one is a statement about what a construction preserves and an algorithm realizing it, which is why it left the metatheory and became infrastructure — Z3, CVC5, Yices, and every program verifier built on them are running step 1 through step 4. The mechanism is worth stating against the modal results: products of modal logics become undecidable because the two relations address one plane, and Nelson–Oppen combinations stay decidable because disjoint signatures give the two theories nothing to address in common but an equivalence relation on finitely many variables. The interface is deliberately impoverished, and the impoverishment is the theorem. Set beside E-connections, which buy decidability by keeping domains disjoint, and Feferman–Vaught, which buys it by making coordinates independent, the pattern is one thing said three ways: a combination transfers when the components cannot see enough of each other to encode a grid.

Applies to. SMT solving — the combination of theory solvers for arrays, bitvectors, linear arithmetic, uninterpreted functions, and datatypes inside a single DPLL(T) architecture. Program verification, since a verification condition mixes arithmetic, arrays, and function symbols and no single decision procedure covers it. Compiler optimization and static analysis. Symbolic execution. Theorem prover integration generally, where the point is to use several specialized procedures without merging them.

Limitations. Disjoint signatures — the hypothesis that makes the theorem true and that real problems violate constantly, whenever two theories both want to mention the integers. The relaxations (Ghilardi, polite and shiny theories) each buy back part of the generality under conditions that must be checked per theory, and none is the general result. Stable infiniteness excludes theories with only finite models, which is why bitvectors needed separate treatment. Non-convexity makes the procedure exponential in shared variables, and the theories that matter most in verification are the non-convex ones. Quantifiers are outside the theorem entirely: it decides quantifier-free satisfiability, and every quantified extension in practice is a heuristic.

© 2026 Lingenic LLC