SAT Solver Verification

swMATH ID: 28831
Software Authors: Filip Maric
Description: 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.
Homepage: https://www.isa-afp.org/entries/SATSolverVerification.html
Dependencies: Isabelle
Related Software: Archive Formal Proofs; Chaff; Isabelle/HOL; MiniSat; BerkMin; SATO; Isabelle; PicoSAT; AVATAR; IsaFoL; Locales; versat; Sledgehammer; z3; VAMPIRE; OCaml; Imperative Refinement; Completeness theorem; DPT; Autoref
Referenced in: 5 Publications

Referenced in 1 Field

5 Computer science (68-XX)

Referencing Publications by Year