Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/520
Title: Formal correctness proof for dPLL procedure
Authors: Marić, Filip 
Janičić, Predrag 
Affiliations: Informatics and Computer Science 
Informatics and Computer Science 
Keywords: DPLL procedure;Formal proofs;Isabelle;Isar;SAT problem
Issue Date: 1-Jan-2010
Journal: Informatica
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. © 2010 Institute of Mathematics and Informatics.
URI: https://research.matf.bg.ac.rs/handle/123456789/520
ISSN: 08684952
Appears in Collections:Research outputs

Show full item record

SCOPUSTM   
Citations

9
checked on Dec 18, 2024

Page view(s)

23
checked on Dec 23, 2024

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.