Abstract DPLL and Abstract DPLL modulo theories

Abstract

We introduce Abstract DPLL, a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as non-chronological backtracking or clause learning. This allows one to formally reason about practical DPLL algorithms in a simple way. In the second part of this paper we extend the framework to Abstract DPLL modulo theories. This allows us to express - and formally reason about - state-of-the-art concrete DPLL-based techniques for satisfiability modulo background theories, such as the different lazy approaches, or our DPLL(T) framework. © Springer-Verlag Berlin Heidelberg 2005.