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 |
| Rank: | M21 |
| 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 firs... |
| URI: | https://research.matf.bg.ac.rs/handle/123456789/520 |
| ISSN: | 08684952 |
| Appears in Collections: | Research outputs |
Show full item record
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.