Formal Verification of Modern SAT Solvers

Title:	Formal Verification of Modern SAT Solvers
Author:	Filip Maric
Submission date:	2007-07-23
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.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

Older releases: