Scott Cotton (Verimag), Satisfiability modulo theory chains with DPLL(T)

This work extends the DPLL(T) framework for satisfiability modulo theories to address richer theories by means of increased flexibility in the interaction between the propositional and theory-specific solvers. We decompose a rich theory into a chain of increasingly more complex subtheories, and define a corresponding regiment of propagation which favors the simpler subtheories using two mechanisms. First, subtheory propagation is prioritized so that more expensive propagation is avoided whenever possible. Second, constraints are filtered along the path from simpler to more complex propagation, thus easing the task of propagation for each subtheory. We present this regiment formally in a refined abstract DPLL(T) system and provide a concrete algorithmic skeleton.