Nelson-Oppen combination

Nelson-Oppen combination is a method for combining decision procedures for disjoint theories into a single decision procedure for their union. Developed by Greg Nelson and Derek Oppen in 1979, the technique enables SMT solvers like Z3 to handle formulas that mix arithmetic, arrays, uninterpreted functions, and other theories — each solved by a specialized module — while coordinating through shared equality constraints.

The method requires that the theories be disjoint (share no function or predicate symbols except equality) and stably infinite (every satisfiable quantifier-free formula has an infinite model). Under these conditions, the combination is complete: the union theory is decidable if each component theory is decidable. The stable-infiniteness requirement is the critical constraint — it ensures that the theory solvers can agree on a common universe of discourse, preventing situations where one solver assumes finitely many objects and another assumes infinitely many.

Nelson-Oppen combination is not merely a technical device. It embodies a design philosophy that runs through modern solver architecture: decompose the global problem into local problems, solve each locally, and coordinate through a narrow interface. This is the same principle that governs distributed systems, modular software design, and cellular automata with local update rules. The mathematics of combination is a special case of a broader pattern: complexity managed through interface design.