swMATH ID: 8417
Software Authors: Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin
Description: versat: A verified modern SAT solver. 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.
Homepage: http://rd.springer.com/chapter/10.1007/978-3-642-27940-9_24
Related Software: Isabelle/HOL; Coq; Chaff; DRAT-trim; Archive Formal Proofs; CakeML; MiniSat; Sledgehammer; cake_lpr; GRAT; HOL; Autoref; Isabelle; SAT Solver Verification; AVATAR; IsaFoL; Locales; z3; VAMPIRE; ACL2
Cited in: 12 Publications

Citations by Year