Combining Decision Procedures with the Nelson–Oppen Method

A program verification obligation rarely stays inside one theory. A single formula may constrain an integer index, an array read, and a function application whose body is unknown. Each of those fragments has its own decision procedure, and the combination problem is to decide the conjunction without giving up the guarantees that made each fragment decidable in the first place. The Nelson–Oppen method answers that question, and its preconditions explain why some combinations work and others do not.

Purification: one literal, one theory

The first step is syntactic. Given a quantifier-free formula over a mixed signature, rewrite it so that every literal mentions symbols from exactly one theory. The rewrite introduces fresh variables for subterms that belong to another theory.

Consider the formula f(x + 1) = y ∧ y ≤ 3, where f is an uninterpreted function symbol, + belongs to arithmetic, and x, y are integer variables. The term x + 1 is arithmetic, but it appears as an argument to f, which is not. Introduce a fresh variable v and split:

• v = x + 1 (arithmetic)
• f(v) = y (uninterpreted functions with equality)
• y ≤ 3 (arithmetic)

The purified formula is equisatisfiable with the original: any model of the original extends to a model of the purified version by giving v the value of x + 1, and any model of the purified version restricts to one of the original by substituting. The purification adds one variable per alien subterm, so its size is linear in the original formula’s size, and the transformation is computable in linear time with a bottom-up traversal that tracks each subterm’s theory.

Purification alone is not enough, because the fresh variables are shared between theories. The arithmetic solver can derive v = 4, and the equality solver must then know that f(4) = y. Communication between the procedures is the second half of the method.

Equality propagation as the only interface

The Nelson–Oppen architecture runs each theory’s decision procedure as a black box that answers satisfiability questions about conjunctions of literals in its own signature. The procedures communicate only through equalities between shared variables. No procedure inspects another’s formula, and no procedure is modified.

The loop is:

1. Each procedure receives its own set of literals, with all shared variables treated as uninterpreted constants.
2. Each procedure reports whether its set is satisfiable, and if so, which equalities between shared variables hold in all its models.
3. Any equality derived by one procedure is added as a fact to every other procedure that shares those variables.
4. Repeat until no new equality appears. If any procedure reports unsatisfiable at any point, the whole conjunction is unsatisfiable. If the loop reaches a fixpoint with all procedures satisfiable, the conjunction is satisfiable.

The termination argument is simple: the set of possible equalities between the finitely many shared variables is finite, each iteration adds at least one new equality or stops, and no equality is ever removed. The number of iterations is bounded by the number of shared variables squared.

The completeness argument is the substantive one. It requires that the theories be stably infinite: every quantifier-free formula satisfiable in the theory has a model whose domain is infinite. Under that condition each procedure’s model can be taken to have a countably infinite domain, so there are always enough domain elements to accommodate every variable that must stay distinct. The equality information shared between the procedures is then enough to glue their models into a single model of the combined formula: equalities partition the shared variables, and each theory’s model can be built to agree on each partition class and to realise that partition with distinct incomparable elements.

Stable infiniteness is not a technical convenience. It is what makes the gluing possible, and theories that violate it break the method.

Why integer arithmetic is the awkward partner

Linear integer arithmetic is decidable, so it looks like a natural component. It is stably infinite: its models include arbitrarily large finite domains, so any satisfiable formula can be satisfied in an infinite model. But it is not convex, and that property, not stable infiniteness, decides whether the plain propagation loop is complete.

A theory is convex when a conjunction of literals that implies a disjunction of equalities between variables always implies one of the disjuncts. The reals are convex in this sense. The integers are not, and the example is small.

Let S be the integer constraints 1 ≤ x ≤ 2 ∧ y = 1 ∧ z = 2 over shared variables x, y, z, and let T be a partner theory that requires x ≠ y ∧ x ≠ z. Together they are unsatisfiable: S forces x into {1, 2}, and each of those values is excluded by T. Over the reals the same S would be satisfiable with x = 1.5, so integer arithmetic is exactly what makes the refutation necessary. But the propagation loop cannot see it. The arithmetic solver is satisfiable and reports no equality implied between shared variables, which is correct: satisfiable S has models where x = 1 and models where x = 2, so x = y holds in none of them and x = z in none. The partner solver is satisfiable on its own, since nothing in T fixes x to a value in {1, 2}. Both report satisfiable, no equality is ever propagated, and the loop reaches a fixpoint at a conjunction that has no model.

The repair is case splitting over arrangements. The combination guesses a partition of the shared variables into those forced equal and those forced distinct, and asserts it as literals before rerunning the loop. In the example, the arrangement {x ≠ y, x ≠ z} plus S is refuted by the arithmetic solver, and the arrangements that identify x with y or with z are refuted by T, so all arrangements fail and the conjunction is correctly reported unsatisfiable.

The number of arrangements is the number of partitions of the shared variables, which is the n-th Bell number and grows faster than exponentially in n, so the guesses are not enumerated blindly. A non-convex theory reports the disjunctions of equalities it implies, and the search branches only on those. Here the arithmetic solver reports x = y ∨ x = z, giving two branches instead of the full set of partitions.

This is why an SMT solver’s performance on mixed integer and real problems can differ so sharply from its performance on purely real ones. The arithmetic reasoning itself is polynomial for linear real constraints and NP-complete for linear integer constraints; the combination layer adds a further source of branching on top of that. Integer constraints are the usual source of that branching, because a bounded integer variable contributes a finite case split that a real variable does not.

Congruence closure as the equality engine

The uninterpreted-function component is worth examining because it is the piece every combination needs and its output is exactly the interface the method consumes.

Congruence closure maintains a partition of terms into equivalence classes, with the invariant that if two terms are in the same class then they are known equal. Two operations modify the partition: merging two classes (asserting an equality) and querying whether two terms are equal. A merge can trigger further merges by congruence: if f(a) and f(b) are both terms and a, b become equal, then f(a) and f(b) must be merged. The process repeats until no new congruence applies.

The efficient implementation uses a union-find structure over term indices, plus a signature table that maps each function symbol and tuple of class representatives to the term that is the class representative for that application. When two classes merge, the signatures of the applications whose arguments mention either class are looked up and any collision produces a new merge, and each merge is charged to a term whose class changed, so the work is bounded by the number of terms times a logarithmic factor from the union-find operations.

class Congruence:
    """Terms are hashable: ('f', (arg1, arg2)) applies f; a string is a leaf."""
    def __init__(self):
        self.parent, self.terms = {}, []   # term -> rep, and insertion order

    def find(self, t):
        self.parent.setdefault(t, t)
        while self.parent[t] != t:
            self.parent[t] = self.parent[self.parent[t]]   # path halving
            t = self.parent[t]
        return t

    def key(self, t):
        """Symbol plus argument representatives, recomputed so keys never stale."""
        if isinstance(t, str):
            return self.find(t)
        sym, args = t
        return (sym, tuple(self.find(a) for a in args))

    def add(self, term):
        self.terms.append(term)
        self._close()

    def merge(self, a, b):
        ra, rb = self.find(a), self.find(b)
        if ra != rb:
            self.parent[rb] = ra
            self._close()

    # Each join invalidates every key, so the search restarts from scratch;
    # a near-linear implementation keeps a use list per class instead.
    def _close(self):
        groups = {}
        for t in self.terms:
            groups.setdefault(self.key(t), []).append(t)
        for group in groups.values():
            for other in group[1:]:
                if self.find(group[0]) != self.find(other):
                    self.parent[self.find(other)] = self.find(group[0])
                    return self._close()

The restart after each join is what makes the code short rather than fast: every join re-derives every key, so the total work is quadratic in the number of terms in the best case and worse once the recursive restarts are counted. The property it demonstrates is the one that matters, namely that merging the classes of a and b forces f(a) and f(b) into one class, and then forces g(f(a)) and g(f(b)) together in turn. A production implementation avoids the restart by keeping, for each class, a list of the application terms whose arguments mention it, so only those terms are revisited.

Where the method fails

Four failure modes account for most of the practical difficulty with combined decision procedures.

Non-stable theories. A theory with a finite domain, or one whose satisfiable formulas can force a bounded domain, may admit formulas that are satisfiable only in models too small to merge with its partner. The theory of a two-element domain is the standard example: it is decidable, it has a satisfiable formula requiring exactly two elements, and it has no infinite model. Combine it with a theory over the same shared variables whose satisfiable formulas require three distinct elements. The conjunction is unsatisfiable, since the shared variables would need three values while the two-element theory allows two, yet both components are separately satisfiable, so the propagation loop can reach a fixpoint and report satisfiable when it is not. Sorted versions of the method handle these cases, at the cost of additional bookkeeping about which elements each theory’s domain owns.

Non-convexity. As with integer arithmetic, the loop must be extended with case splits, and the branching is the dominant cost. A solver that reports “unknown” on a mixed integer problem is often hitting this wall rather than failing to reason.

Missing explanations. In a real solver the components do not merely report satisfiability; they report conflicts, sets of literals that are jointly inconsistent, so the search can backtrack intelligently instead of enumerating branches. A theory solver that can only say “unsatisfiable” forces the search to learn nothing from the failure, and the combination degenerates into blind enumeration. The quality of conflict explanations, not the decision procedure itself, often determines whether the combined solver scales.

Signature overlap. The method assumes the theories’ signatures intersect only in the shared variables and in equality. A symbol that belongs to two theories — an arithmetic operation that also appears in a theory of arrays, for instance — violates that disjointness condition, and the completeness proof for the propagation loop does not apply. Implementations either treat such symbols as belonging to one theory and rewrite the other’s occurrences in terms of it, or fall back on a combination method designed for overlapping signatures.

What the combination buys

The value of the method is modularity. Each theory’s decision procedure can be developed, proved correct, and optimised independently, and the combination is a thin layer of equality propagation on top. This is why an SMT solver can offer arithmetic, arrays, bit-vectors, and uninterpreted functions without a monolithic decision procedure for the union: the union’s decidability is inherited from the components plus the preconditions.

The price is that the preconditions are not free. Stable infiniteness, convexity or explicit splitting, and disjoint signatures are properties of the combination, not of any single theory, and a theory that is perfectly well behaved alone can be unusable in a combination. That is the same trade visible throughout this subject: Presburger Arithmetic and the Decidable Side of Number Theory gives a decision procedure for one fragment, and Trakhtenbrot’s Theorem and the Finite Model Boundary shows what happens when the fragment is widened. Combination sits between them: it widens the fragment without widening any component, and the widening is exactly as sound as its preconditions allow.