Abstract DPLL and Abstract DPLL Modulo Theories

DPLL and DPLL Modulo Theories Robert Nieuwenhuis , Albert Oliveras , and Cesare Tinelli 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.

• Type: Conference
• Year: 2004
• Where: LPAR
• Authors: Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
• Keywords: Abstract DPLL, Abstract Rule-based Formulation, Dpll Modulo Theories, LPAR 2004