Formal Correctness Proof for DPLL Procedure

Article type: Research Article

Authors: Marić, Filip | Janičić, Predrag

Affiliations: Faculty of Mathematics, University of Belgrade, Studentski trg 16, Belgrade, Serbia, e-mail: filip@matf.bg.ac.rs; janicic@matf.bg.ac.rs

Abstract: 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.

Keywords: SAT problem, DPLL procedure, formal proofs, Isabelle, Isar

Journal: Informatica, vol. 21, no. 1, pp. 57-78, 2010