1. Research with MATF
  2. MATF
  3. Research outputs
Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/520
DC FieldValueLanguage
dc.contributor.authorMarić, Filipen_US
dc.contributor.authorJaničić, Predragen_US
dc.date.accessioned2022-08-13T10:14:43Z-
dc.date.available2022-08-13T10:14:43Z-
dc.date.issued2010-01-01-
dc.identifier.issn08684952en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/520-
dc.description.abstractThe 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.en_US
dc.language.isoenen_US
dc.publisherVilnius : Vilnius University Pressen_US
dc.relation.ispartofInformaticaen_US
dc.subjectDPLL procedureen_US
dc.subjectFormal proofsen_US
dc.subjectIsabelleen_US
dc.subjectIsaren_US
dc.subjectSAT problemen_US
dc.titleFormal correctness proof for dPLL procedureen_US
dc.typeArticleen_US
dc.identifier.doi10.15388/informatica.2010.273-
dc.identifier.scopus2-s2.0-77949796445-
dc.identifier.isi000276558800005-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/77949796445-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.issn0868-4952en_US
dc.description.rankM21aen_US
dc.relation.firstpage57en_US
dc.relation.lastpage78en_US
dc.relation.volume21en_US
dc.relation.issue1en_US
item.openairetypeArticle-
item.languageiso639-1en-
item.grantfulltextnone-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.fulltextNo Fulltext-
item.cerifentitytypePublications-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-7219-6960-
crisitem.author.orcid0000-0001-8922-4948-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

9
checked on Dec 3, 2025

Page view(s)

24
checked on Jan 19, 2025

Google ScholarTM

Check

Altmetric

Altmetric


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