[isabelle] new AFP entry: SATSolverVerification
We are pleased to announce the availability of a new entry in the
Archive of Formal Proofs at [http://afp.sf.net]:
Formal Verification of Modern SAT solvers
by Filip Maric
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and