Email Gateway (Aug 18 2022 at 12:15): Email Gateway (Aug 18 2022 at 12:15):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
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.
Cheers,
Gerwin
Last updated: May 03 2024 at 08:18 UTC