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. © 2012 Springer-Verlag.
CITATION STYLE
Oe, D., Stump, A., Oliver, C., & Clancy, K. (2012). Versat: A verified modern SAT solver. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7148 LNCS, pp. 363–378). https://doi.org/10.1007/978-3-642-27940-9_24
Mendeley helps you to discover research relevant for your work.