Scott Cotton and Oded Maler
Satisfiability Modulo Theory Chains with DPLL(T) (2006)
Satisfiability Modulo Theory Chains with DPLL(T) (2006)
TR-2006-4.pdf
Keywords:
Abstract: We extend the DPLL(T) framework for satisfiability modulo theories to address richer theo- ries 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 sub- theories, and define a corresponding propagation strategy which favors the simpler subtheo- ries 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.
