Skip to main content

Boolean Satisfiability Solvers and Their Applications in Model Checking

Author(s): Vizel, Y; Weissenbacher, G; Malik, Sharad

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1p20c
Full metadata record
DC FieldValueLanguage
dc.contributor.authorVizel, Y-
dc.contributor.authorWeissenbacher, G-
dc.contributor.authorMalik, Sharad-
dc.date.accessioned2020-04-01T13:22:54Z-
dc.date.available2020-04-01T13:22:54Z-
dc.date.issued2015-8-26en_US
dc.identifier.citationVizel, Y, Weissenbacher, G, Malik, S. (2015). Boolean Satisfiability Solvers and Their Applications in Model Checking. Proceedings of the IEEE, 103 (2021 - 2035. doi:10.1109/JPROC.2015.2455034en_US
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1p20c-
dc.description.abstractBoolean satisfiability (SAT) - the problem of determining whether there exists an assignment satisfying a given Boolean formula - is a fundamental intractable problem in computer science. SAT has many applications in electronic design automation (EDA), notably in synthesis and verification. Consequently, SAT has received much attention from the EDA community, who developed algorithms that have had a significant impact on the performance of SAT solvers. EDA researchers introduced techniques such as conflict-driven clause learning, novel branching heuristics, and efficient unit propagation. These techniques form the basis of all modern SAT solvers. Using these ideas, contemporary SAT solvers can often handle practical instances with millions of variables and constraints. The continuing advances of SAT solvers are the driving force of modern model checking tools, which are used to check the correctness of hardware designs. Contemporary automated verification techniques such as bounded model checking, proof-based abstraction, interpolation-based model checking, and IC3 have in common that they are all based on SAT solvers and their extensions. In this paper, we trace the most important contributions made to modern SAT solvers by the EDA community, and discuss applications of SAT in hardware model checking.en_US
dc.format.extent2021 - 2035en_US
dc.language.isoen_USen_US
dc.relation.ispartofProceedings of the IEEEen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.titleBoolean Satisfiability Solvers and Their Applications in Model Checkingen_US
dc.typeJournal Articleen_US
dc.identifier.doidoi:10.1109/JPROC.2015.2455034-
dc.date.eissued2015-8-26en_US
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/journal-articleen_US

Files in This Item:
File Description SizeFormat 
Boolean Satisfiability Solvers and Their Applications in Model Checking.pdf422.25 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.