Versat: A verified modern SAT solver

29Citations
Citations of this article
11Readers
Mendeley users who have this article in their library.
Get full text

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. © 2012 Springer-Verlag.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free