DPLL(T)

also: dpll t, theory combination

The standard architecture for an SMT solver: a CDCL core treats each theory atom as a boolean variable and searches as usual, while a theory solver checks each candidate assignment for theory consistency and hands back an explanation when it fails. The explanation becomes a learned clause, so the boolean search is what drives progress.

The standard architecture for an SMT solver, and a small one: keep a CDCL core and give it a theory solver to consult. Each distinct theory atom becomes a boolean variable, the core searches over those as usual, and the theory checks whether the assignment it proposes is consistent.

1. CDCL assigns a set of theory atoms true or false
2. assert them into the theory solver
3. consistent?   -> keep searching, or report SAT if the assignment is total
   inconsistent? -> ask for an explanation: a subset that already conflicts
4. negate the explanation, add it as a learned clause, backjump
5. repeat

Step 4 is what makes the architecture work rather than merely terminate. The explanation becomes an ordinary clause over the boolean variables, so all of CDCL's machinery, learning, backjumping, activity, applies to theory conflicts without knowing anything about the theory.

Smaller explanations are strictly better: a conflict set of two atoms prunes far more of the search space than the full assignment does. That is the single most important property asked of a theory solver, ahead of raw speed.

SMT · Theory solver · CDCL

• Implementing SAT in OCaml Part 3From SAT to SMT: the DPLL(T) architecture, reusing conflict-driven learning for theory conflicts, and a union-find equality theory.