Abstract: |
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.
|
BibTeX: |
@article{SATSolverVerification-AFP,
author = {Filip Maric},
title = {Formal Verification of Modern SAT Solvers},
journal = {Archive of Formal Proofs},
month = jul,
year = 2008,
note = {\url{http://isa-afp.org/entries/SATSolverVerification.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|