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 7 articles )
Showing results 1 to 7 of 7.
- Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan: Efficient, verified checking of propositional proofs (2017)
- Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
- 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)
- Philipp, Tobias: An expressive model for instance decomposition based parallel SAT solvers (2015)
- Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun.: Mechanical verification of SAT refutations with extended resolution (2013)
- Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin: versat: a verified modern SAT solver (2012)