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.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
- 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)