Generalizing DPLL to Richer Logics

14 years 1 months ago
Generalizing DPLL to Richer Logics
The DPLL approach to the Boolean satisfiability problem (SAT) is a combination of search for a satisfying assignment and logical deduction, in which each process guides the other. We show that this approach can be generalized to a richer class of theories. In particular, we present an alternative to lazy SMT solvers, in which DPLL is used only to find propositionally satisfying assignments, whose feasibility is checked by a separate theory solver. Here, DPLL is applied directly to the theory. We search in the space of theory structures (for example, numerical assignments) rather than propositional assignments. This makes it possible to use conflict in model search to guide deduction in the theory, much in the way that it guides propositional resolution in DPLL. Some experiments using linear rational arithmetic demonstrate the potential advantages of the approach.
Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagi
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where CAV
Authors Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv
Comments (0)