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.

Ich entwickele ein formales Framework für propositionale Erfüllbarkeit mit der conflict-driven clause learning (CDCL) Prozedur in dem Beweisassistenten Isabelle/HOL. Das Framework ermöglicht es, Metatheoreme zu beweisen und mit Varianten zu experimentieren, wie den Davis–Putnam–Logemann– Loveland Kalkül. Ein Schwerpunkte meiner Arbeit sind die Regeln für forget, restart und den Verfeinerungsansatz. Ich benutzte die Formalisierung um drei Erweiterungen zu entwickeln. Zuerst, eine inkrementele Version von CDCL. Zweitens, habe ich ein optimierendes CDCL (OCDCL) verifiziert. Für eine gegebene Kostenfunktion auf Literale, berechnet OCDCL ein model mit minimalen Kosten. Schließlich, habe ich an Modelüberdeckung gearbeitet. Dank dem Framework sind die Erweiterungen einfach zu entwickeln. Durch mehrere Verfeinerungsschritte verbinde ich das abstrakte CDCL Kalkül erst zu einem konkreterem Kalkül, dann zu einem SAT solver in einer simplen funktionalen Sprache, bis zu einem imperativen SAT solver mit totale Korrektheit. Die imperative Version enthält die two-watched-literals Datenstruktur und andere Optimierungen von modernen SAT Solvern. Ich benutze das Isabelle Refinement Framework, um die mühsamsten Schritte zu automatisieren. Später habe ich diese Formalisierung mit anderen Optimierungen erweitert, wie blocking literals and die Nutzung von Machinwörtern so lange wie möglich, before unbegrentzte Zahlen benutzt werden, um Vollständigkeit zu haben.