Generalizing DPLL to richer logics

Abstract

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. © 2009 Springer Berlin Heidelberg.