Formalization of Abstract State Transition Systems for SAT

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