Formal Correctness Proof for DPLL Procedure

10 years 2 months ago
Formal Correctness Proof for DPLL Procedure
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. Key words: SAT problem, DPLL procedure, formal proofs, Isabelle, Isar
Filip Maric, Predrag Janicic
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Authors Filip Maric, Predrag Janicic
Comments (0)