Hauptseminar - Themenvorschläge
Die beiden großen Themenbereiche des Hauptseminars SAT-Solving und Beweisassistenten.
Literatur
- Armin Bier, Marijn Heule, and Hans van Maaren, 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.
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.
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.
