SAT solvers are automatic decision procedures for the propositional satisfiability problem; they play an important role in planning, scheduling, optimization, and especially the formal verification of hardware and software systems. Thus, verifying the correctness of SAT solvers and deriving provably correct solvers has become of major interest.

This paper contributes a formal framework for the theory of conflict-driven clause learning (CDCL) underlying modern SAT solvers. The theory is elaborated with the Isabelle/HOL proof assistant, and an abstract algorithm in the form of a state transition system is formulated and verified. By a sequence of refinements, the algorithm is concretized and various optimizations are incorporated; the Isabelle code generator translates the resulting functional algorithm into actually executable code. Finally, an imperative implementation is derived that makes use of efficient mutable data structures, yielding a reasonably efficient and provably correct SAT solver.

The present work was performed within a period of ten months and has yielded about 28000 lines of Isabelle text; it is part of an effort to formalize the content of a forthcoming textbook on automated reasoning (Blanchette et al. actually identify a major mistake in the draft of the book). Apart from the details of the presented methodology, it is most interesting to read about the insights the authors gained during their formalization work. These insights are also relevant to researchers in other application domains who are interested in a thorough understanding of their theories and the correctness of their algorithms.