English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Formalization of Logical Calculi in Isabelle/HOL

Fleury, M. (2020). Formalization of Logical Calculi in Isabelle/HOL. PhD Thesis, Universität des Saarlandes, Saarbrücken. doi:10.22028/D291-30179.

Item is

Files

show Files

Locators

show
hide
Description:
-
OA-Status:
Green

Creators

show
hide
 Creators:
Fleury, Mathias1, 2, Author           
Weidenbach, Christoph1, Advisor                 
Biere, Armin3, Referee
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
3External Organizations, ou_persistent22              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2020-01-1820202020
 Publication Status: Issued
 Pages: 169 p.
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: Fleuryphd2019
DOI: 10.22028/D291-30179
URN: urn:nbn:de:bsz:291--ds-301796
Other: hdl:20.500.11880/28722
 Degree: PhD

Event

show

Legal Case

show

Project information

show

Source

show