versat 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 all top 5 Cited by 25 Authors 4 Heule, Marijn J. H. 2 Blanchette, Jasmin Christian 2 Fleury, Mathias 2 Lammich, Peter 2 Weidenbach, Christoph 2 Wetzler, Nathan D. 1 Baek, Seulkee 1 Berger, Ulrich 1 Ciobâcă, Ştefan 1 Clancy, Kevin 1 Hunt, Warren A. jun. 1 Hunt, Warren jun. 1 Iordache, Viorel 1 Kaufmann, Matt 1 Lawrence, Andrew 1 Lindauer, Marius 1 Manthey, Norbert 1 Myreen, Magnus O. 1 Nordvall Forsberg, Fredrik 1 Oe, Duckki 1 Oliver, Corey 1 Philipp, Tobias 1 Seisenberger, Monika 1 Stump, Aaron 1 Tan, Yong Kiam Cited in 2 Serials 2 Journal of Automated Reasoning 2 Logical Methods in Computer Science Cited in 2 Fields 11 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year