Sciweavers

Share
LPAR
2004
Springer

Abstract DPLL and Abstract DPLL Modulo Theories

10 years 4 months ago
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.
Robert Nieuwenhuis, Albert Oliveras, Cesare Tinell
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LPAR
Authors Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
Comments (0)
books