Skip to Main content Skip to Navigation

Formalization of Logical Calculi in Isabelle/HOL

Mathias Fleury 1, 2, 3 
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Complete list of metadata

Cited literature [161 references]  Display  Hide  Download
Contributor : Mathias Fleury Connect in order to contact the contributor
Submitted on : Saturday, October 10, 2020 - 7:37:51 AM
Last modification on : Thursday, January 20, 2022 - 5:26:13 PM
Long-term archiving on: : Monday, January 11, 2021 - 6:02:36 PM


Files produced by the author(s)


  • HAL Id : tel-02963301, version 1


Mathias Fleury. Formalization of Logical Calculi in Isabelle/HOL. Logic in Computer Science [cs.LO]. Universität des Saarlandes Saarbrücken, 2020. English. ⟨tel-02963301⟩



Record views


Files downloads