×

zbMATH — the first resource for mathematics

Formal correctness proof for DPLL procedure. (English) Zbl 1209.68514
Summary: The DPLL procedure for the SAT problem is one of the fundamental algorithms in computer science, with many applications in a range of domains, including software and hardware verification. Most of the modern SAT solvers are based on this procedure, extending it with different heuristics. In this paper we present a formal proof that the DPLL procedure is correct. As far as we know, this is the first such proof. The proof was formalized within the Isabelle/Isar proof assistant system. This proof adds to the growing body of formalized mathematical knowledge and it also provides a number of lemmas relevant for proving correctness of modern SAT and SMT solvers.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: Link