Hauptseminar - Themenvorschläge
Die beiden großen Themenbereiche des Hauptseminars SAT-Solving und Beweisassistenten.
Literatur
- Armin Biere, Marijn Heule, and Hans van Maaren, Toby Walsh, eds. Handbook of satisfiability. Amsterdam IOS Press 2021. Sie können es über unsere Bibliothek hier online lesen und auch irgendwie herunterladen.
- Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg, The hitchhiker's guide to logical verification, Vrije Universiteit Amsterdam (2021)
SAT und SAT-Solving
Resolution. Dies ist ein "Beweissystem", mit dem man z.B. die Unerfüllbarkeit einer CNF-Formel zeigen kann. Die Struktur der Beweise ist eng mit DPLL-Algorithmen verbunden, daher sollten wir Resolution verstehen, um SAT-Solver und Techniken wie CDCL zu verstehen.
Ihr Vortrag sollte Boolesche Resolution und ihre Varianten wie Baumresolution und reguläre Resolution behandeln und die Vollständigkeit der Resolution beinhalten. Irgendeine Form von unterer Schranke sollte dabei sein, z.B. für das Pigeon Hole Principle oder für Tseitin-Formeln.
- Als Material können Sie Kapitel 7 im Handbook of Satisfiability nehmen oder kontaktieren mich für alternatives Material.
- Kapitel 15 im Handbook of Satisfiability, also Proofs of Unsatisfiablity, könnte Stoff für einen zweiten Vortrag zu diesem Thema liefern. So wie ich es überblicke, geht es in Kapitel 7 mehr um die Theorie der Beweiskomplexität und in Kapitel 15, wie den solche Beweise bei SAT-Solvern aussehen.
Conflict-driven clause learning (CDCL). CDCL ist ein Paradigma, DPLL-Algorithmen (also splitting-basierte SAT-Algorithmen) effizienter macht, in dem man neue Klauseln "lernt", um in Zukunft Sackgassen zu vermeiden (soweit mein in diesem Feld noch etwas rudimentäres Verständnis). CDCL bildet die Grundlage der meisten (aller?) SAT-Solver, daher sollte dieses Thema unbedingt Teil des Seminars sein.
Als Material können Sie Kapitel 4 im Handbook of Satisfiability nehmen, zumindest als Startpunkt.
Weiteres über SAT-Solver. Im Thema CDCL geht es ja bereits konkret um SAT-Solver. Wenn Interesse besteht, noch tiefer in die Materie einzusteigen, benötigen wir einen weiteren Vortrag zu dem Thema. Basis könnte z.B. Kapitel 5, Look-Ahead Based SAT Solvers oder Kapitel 9, Preprocessing in SAT Solvers im Handbook of Satisfiability sein.
Anwendungen von SAT-Solvern. Darum geht es bei SAT-Solvern ja: dass man sie anwenden kann, um andere Probleme zu lösen. Als Ausgangspunkt würde ich hier Kapitel 19 (Planning and SAT) und Kapitel 20 (Software Verification) empfehlen, allerdings kann es sein, dass Sie beim Lesen auf eine andere interessantere Anwendung in der Literatur stoßen.
Ihr Vortag sollte das Problem (also den Anwendungsbereich) klar darstellen und erläutern, wie dies mit SAT formuliert und gelöst wird. Da könnte es hilfreich sein, auch auf CNF Encodings (Kapitel 2) einzugehen (aber vielleicht werde ich in den ersten Wochen des Seminars auch darüber sprechen).
Beweisassistenten
In diesem Teil werden wir Lean kennen und nutzen lernen. Einen Literaturvorschlag finden Sie oben. Konkrete Themenvorschläge muss ich noch ausarbeiten. Vorschläge von Ihrer Seite sehr willkommen. Im Moment ist meine Vorstellung, dass wir gemeinsam (unter Johannes Tantows oder meiner Leitung) uns in Lean einarbeiten. Die Seminarvorträge gehen dann auf einzelne Themen, Theorien, Beweise ein und wie man sie in Lean formalisiert. Hier folgen einige Themenvorschläge. Allerdings sind die meistens nicht in Lean (eines ist in Lean3, einer älteren, nicht kompatiblen Version). Aufgabe wäre es, die Formalisierung vorzustellen und teilweise in Lean nachzubauen.
Türme von Hanoi. Optimale Lösungen zu Varianten der Türme von Hanoi in Rocq. Proof Pearl : Playing with the Tower of Hanoi Formally
Cook-Levin-Theorem in Coq. Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. Des Inhalts wegen natürlich für uns interessant. Eventuell recht aufwändig. Lässt es sich in zwei Teile teilen?
Closure Properties of General Grammars - Formally Verified. Da geht es um formale Grammatiken. Allerdings ist es in Lean 3 geschrieben, was mit dem aktuellen Lean nicht mehr kompatibel ist. Aus theoretischer Sicht kann man es natürlich immer noch betrachten. Vielleicht Teile davon in der aktuellen Lean-Version nachbauen.
Verschiedene Graphalgorithmen. Hier finden Sie die Publikationsliste von Mohammad Abdulaziz. Er hat verschiedene graphentheoretische Dinge in Isabelle formalisiert. Stöbern Sie mal rum!
