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

• Type: Journal
• Year: 2010
• Where: INFORMATICALT
• Authors: Filip Maric, Predrag Janicic
• Keywords: DPLL Procedure, Formal Proofs, INFORMATICALT 2010, Modern Sat