Satisfiability Modulo Theory Chains with DPLL(T)
Scott Cotton, Oded Maler · 2006
Abstract. We extend 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 propagation strategy 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 strategy formally in a refined abstract DPLL(T) system and provide a concrete algorithmic skeleton with a proof of correctness. 1