  We present a formalization of modern SAT solvers and their properties in a
form of abstract state transition systems. SAT solving procedures are described
as transition relations over states that represent the values of the solver's
global variables. Several different SAT solvers are formalized, including both
the classical DPLL procedure and its state-of-the-art successors. The
formalization is made within the Isabelle/HOL system and the total correctness
(soundness, termination, completeness) is shown for each presented system (with
respect to a simple notion of satisfiability that can be manually checked). The
systems are defined in a general way and cover procedures used in a wide range
of modern SAT solvers. Our formalization builds up on the previous work on
state transition systems for SAT, but it gives machine-verifiable proofs,
somewhat more general specifications, and weaker assumptions that ensure the
key correctness properties. The presented proofs of formal correctness of the
transition systems can be used as a key building block in proving correctness
of SAT solvers by using other verification approaches.
