Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Formal Verification of Modern SAT Solvers

 

Title: Formal Verification of Modern SAT Solvers
Author: Filip Marić (filip /at/ matf /dot/ bg /dot/ ac /dot/ rs)
Submission date: 2008-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.
BibTeX: 
@article{SATSolverVerification-AFP,
  author  = {Filip Marić},
  title   = {Formal Verification of Modern SAT Solvers},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2008,
  note    = {\url{http://isa-afp.org/entries/SATSolverVerification.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document
Browse theories
Download this entry