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.