Skip to Main content Skip to Navigation
Theses

Formalization of Logical Calculi in Isabelle/HOL

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 :
Theses
Complete list of metadatas

Cited literature [161 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-02963301
Contributor : Mathias Fleury <>
Submitted on : Saturday, October 10, 2020 - 7:37:51 AM
Last modification on : Saturday, October 10, 2020 - 11:12:15 AM

File

Fleury-thesis.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02963301, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

104

Files downloads

21