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
dc.relation.ispartofInformaticaen
dc.subjectDPLL procedureen
dc.subjectFormal proofsen
dc.subjectIsabelleen
dc.subjectIsaren
dc.subjectSAT problemen
dc.titleFormal correctness proof for dPLL procedureen_US
dc.typeArticleen_US
dc.identifier.scopus2-s2.0-77949796445-
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.firstpage57en
dc.relation.lastpage78en
dc.relation.volume21en
dc.relation.issue1en
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
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 18, 2024

Page view(s)

23
checked on Dec 24, 2024

Google ScholarTM

Check


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