Campus Event Calendar
Event Entry
What and Who
Formalization of Logical Calculi in Isabelle/HOL
Mathias Fleury
Max-Planck-Institut für Informatik - RG 1
Promotionskolloquium
AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 28 January 2020
10:00
90 Minutes
E1 4
024
Saarbrücken
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, restart and the refinement approach.
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.
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.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/16/2020 15:12 -- Created document.