SAT Solver Verification
SATSolverVerification: Formal Verification of Modern SAT Solvers. This document contains formal correctness proofs of modern SAT solvers. Following (Krstic et al, 2007) and (Nieuwenhuis et al., 2006), solvers are described using state-transition systems. Several different SAT solver descriptions are given and their partial correctness and termination is proved. These include: a solver based on classical DPLL procedure (using only a backtrack-search with unit propagation), a very general solver with backjumping and learning (similar to the description given in (Nieuwenhuis et al., 2006)), and a solver with a specific conflict analysis algorithm (similar to the description given in (Krstic et al., 2007)). Within the SAT solver correctness proofs, a large number of lemmas about propositional logic and CNF formulae are proved. This theory is self-contained and could be used for further exploring of properties of CNF based SAT algorithms.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
- Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
- Marić, Filip; Janičić, Predrag: Formalization of abstract state transition systems for SAT (2011)
- Marić, Filip: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (2010)
- Marić, Filip: Formalization and implementation of modern SAT solvers (2009)