Book chapter
versat: A Verified Modern SAT Solver
Verification, Model Checking, and Abstract Interpretation, pp.363-378
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2012
DOI: 10.1007/978-3-642-27940-9_24
Abstract
This paper presents versat, a formally verified SAT solver incorporating the essential features of modern SAT solvers, including clause learning, watched literals, optimized conflict analysis, non-chronological backtracking, and decision heuristics. Unlike previous related work on SAT-solver verification, our implementation uses efficient low-level data structures like mutable C arrays for clauses and other solver state, and machine integers for literals. The implementation and proofs are written in Guru, a verified-programming language. We compare versat to a state-of-the-art SAT solver that produces certified “unsat” answers. We also show through an empirical evaluation that versat can solve SAT problems on the modern scale.
Details
- Title: Subtitle
- versat: A Verified Modern SAT Solver
- Creators
- Duckki Oe - University of IowaAaron Stump - University of IowaCorey Oliver - University of IowaKevin Clancy - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Verification, Model Checking, and Abstract Interpretation, pp.363-378
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-27940-9_24
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2012
- Academic Unit
- Computer Science
- Record Identifier
- 9984259461902771
Metrics
10 Record Views