b'@phdthesis{Fleuryphd2019,'b'\nTITLE = {Formalization of Logical Calculi in Isabelle/{HOL}},\nAUTHOR = {Fleury, Mathias},\nLANGUAGE = {eng},\nURL = {urn:nbn:de:bsz:291--ds-301796},\nDOI = {10.22028/D291-30179},\nSCHOOL = {Universit{\\"a}t des Saarlandes},\nADDRESS = {Saarbr{\\"u}cken},\nYEAR = {2020},\nDATE = {2020},\nABSTRACT = {I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.},\n}\n'