In the DPLL(T) architecture, what is the division of responsibility between the SAT engine and the theory solver?
AThe SAT engine handles all reasoning; the theory solver only validates the final answer
BThe SAT engine manages the Boolean structure and propositional decisions, while the theory solver checks whether conjunctions of theory literals assigned true by the SAT engine are consistent in the background theory
CThe theory solver runs first to simplify the formula, then the SAT engine solves the simplified version
DThe SAT engine and theory solver operate independently and vote on the result
DPLL(T) treats each theory atom (like x + y > 5 or a[i] = b[j]) as an opaque Boolean variable from the SAT engine's perspective. The SAT engine makes decisions and propagates using standard CDCL. After each propagation round (or periodically), the current set of true theory literals is passed to the theory solver, which checks their joint satisfiability in the background theory. If the theory solver detects inconsistency, it returns a theory conflict clause -- a subset of the literals that are jointly unsatisfiable -- which the SAT engine incorporates as a learned clause, triggering backjumping. This lazy integration allows the SAT engine's powerful Boolean reasoning to handle the combinatorial structure while theory solvers focus on domain-specific consistency.
Question 2 Short Answer
The Nelson-Oppen combination method requires that the individual theories be stably infinite and signature-disjoint. Why is signature disjointness needed?
Think about your answer, then reveal below.
Model answer: Signature disjointness means the theories share no function or predicate symbols (except equality). This ensures each literal belongs unambiguously to exactly one theory, so each theory solver can reason about its own literals independently. The theories communicate only through equalities and disequalities over shared variables that appear in both theories. Without disjointness, a single symbol could have different semantics in different theories, making combination unsound. Stable infiniteness ensures that if a theory finds a model, it can be extended to one with infinitely many elements, which guarantees that the theories can always agree on a shared domain for their combined model.
In practice, some important theory pairs violate strict disjointness (e.g., arrays with integer indices and linear integer arithmetic both interpret integer operations). Modern SMT solvers handle this through extensions to Nelson-Oppen, such as the theory of arrays being formulated to communicate with arithmetic through index equalities. The CVC5 and Z3 implementations use more flexible combination strategies than pure Nelson-Oppen.
Question 3 True / False
SMT solvers can always decide the satisfiability of quantifier-free formulas in supported theories.
TTrue
FFalse
Answer: True
For the standard quantifier-free theories supported by modern SMT solvers -- linear real arithmetic (LRA), linear integer arithmetic (LIA), bitvectors (BV), arrays (with extensionality), uninterpreted functions (EUF) -- satisfiability is decidable. LRA is in polynomial time, LIA is NP-complete, BV is NP-complete, and their combinations remain decidable. However, adding quantifiers generally makes the problem undecidable (first-order arithmetic is undecidable). SMT solvers handle quantifiers heuristically through E-matching and quantifier instantiation, which may not terminate. Nonlinear real arithmetic (NRA) is decidable but doubly exponential; nonlinear integer arithmetic is undecidable.
Question 4 Short Answer
Why do SMT solvers use theory propagation in addition to theory conflict detection?
Think about your answer, then reveal below.
Model answer: Theory propagation allows the theory solver to proactively inform the SAT engine about implied literals, rather than waiting for the SAT engine to guess and then detecting a conflict. For example, if the theory solver knows x < 3 is true and sees the unassigned literal x < 5, it can propagate x < 5 as implied (since x < 3 implies x < 5 in linear arithmetic). This reduces the number of decisions the SAT engine must make and prevents it from exploring branches that the theory already knows are forced. Theory propagation is analogous to unit propagation in pure SAT but operates at the theory level.
Theory propagation was a significant performance improvement over early DPLL(T) implementations that only used theory conflict detection. The original 'lazy' approach would let the SAT engine assign theory literals freely, only intervening on inconsistency. Theory propagation makes the integration more 'eager,' catching implications before the SAT engine wastes decisions on them. The tradeoff is that propagation queries can be expensive for some theories, so solvers tune how aggressively to propagate.