Nelson-Oppen Theory Combination — Brief ☧
"In whom are hid all the treasures of wisdom and knowledge."
— Colossians 2:3 (KJV)
Deep version → | Back to Abstract Interpretation →
Q: Suppose you are planning a road trip. You need a map expert
(which roads connect which cities), a budget expert (can you afford
the gas?), and a time expert (will you arrive before dark?). Each
expert is great at their own domain but knows nothing about the others.
How do you get them to cooperate on a single question — "Can I drive
from A to B for under $50 and arrive by 6 PM?"
A: You let each expert work on their piece, and then you have them
share what they learn about the things they have in common. The map
expert might say "the shortest route goes through city C." The budget
expert uses that to calculate fuel cost. The time expert uses the
route to estimate arrival time. They keep exchanging information until
everyone agrees — or someone declares "impossible."
This is exactly the Nelson-Oppen method: let each specialized
solver (called a "theory") handle its own kind of constraint, and
communicate shared equalities between them. Each expert exchanges
what it has deduced about shared variables until all theories agree.
Q: Where do you actually see this in practice?
A: In SMT solvers like Z3, CVC5, and Yices. "SMT" stands for
Satisfiability Modulo Theories — it means checking whether a formula
is satisfiable, given background knowledge from multiple theories.
An SMT solver might combine:
- A theory of arithmetic (is
x + y > 10?)- A theory of arrays (is
a[i] = a[j]?)- A theory of bit-vectors (does this 32-bit operation overflow?)
- A theory of uninterpreted functions (if
f(x) = f(y), doesx = y?)Nelson-Oppen (and its modern variant DPLL(T)) is the glue that lets
these different solvers work together on a single problem.
Q: What makes this work reliably? Could the experts just go back
and forth forever?
A: The key requirement is convexity: each theory's solver, when
it deduces something about shared variables, produces a single equality
(not a disjunction of possibilities). This guarantees termination. Our
Boolean bitmask domains are convex — when we
intersect two domains, the result is a single, definite domain — so the
method converges cleanly.
Key Concepts
| Concept | Meaning | Our Project |
|---|---|---|
| Theory | Decision procedure for a domain | Bitmask intersector |
| Convexity | Disjunctions not needed | Our Boolean domains are convex |
| Shared variables | Variables in multiple theories | Variables shared between relations |
| Equality propagation | Exchange equalities | Domain refinement via arc consistency |
The table maps each Nelson-Oppen concept to our system, and the correspondence is tighter than it might first appear. Each row of the table represents a principle that directly guides how our constraint solver operates: specialized solvers handle their own domains, shared variables trigger communication between solvers, and the process iterates until all solvers agree.
Connection to our system: Our constraint solver is, in spirit, a Nelson-Oppen
combination operating at hardware speed. Each relation (appendo, membero, etc.) is a "theory" with its own
intersection algorithm: it knows how to prune variable domains based on its specific constraint. When variables are shared
across relations -- which they almost always are in real queries -- we propagate domain refinements between them. If appendo(L, S, Out) prunes the domain of Out, and membero(Out, [1,2,3]) also constrains Out, the refinements from both relations are combined (intersected) and propagated back to each relation's other variables. This exchange continues — exchanging
equalities (domain refinements) until a fixpoint is reached, exactly as Nelson-Oppen prescribes. The convexity of our Boolean domains (intersection always produces a single definite result, never a disjunction) guarantees that this process terminates, and the FPGA's 770,000 operations per second ensures it terminates quickly.
Soli Deo Gloria