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.
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Manthey, Norbert; Lindauer, Marius: Spybug: automated bug detection in the configuration space of SAT solvers (2016)
- Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
- Wetzler, Nathan; Heule, Marijn J.H.; Hunt, Warren A.Jr.: Mechanical verification of SAT refutations with extended resolution (2013)
- Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin: versat: a verified modern SAT solver (2012)