Informatica Logo

INFORMATICA
International Journal

Main Page
Editorial Board
Abstracting/Indexing
Instructions to Authors
Subscription Information


Contents
Author Index
Papers in Production

INFORMATICA, 2010, Vol. 21, No. 1, 57-78
© Institute of Mathematics and Informatics,

ISSN 0868-4952

Formal Correctness Proof for DPLL Procedure

Filip MARIC, Predrag JANICIC

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

To preview Lithuanian abstract see full article text

PDFTo preview full article text in PDF format click here

Get Free ReaderYou could obtain free Acrobat Reader from Adobe


TopTop Copyright © INFORMATICA, Vilnius University Institute of Mathematics and Informatics, 2010