Seminar Algorithmik: Algorithmen in der Aussagenlogik
Inhalt
In diesem Seminar wollen wir einfache Aspekte des Themenbereichs Beweiskomplexität zu Algorithmen in der Aussagenlogik studieren und einige grundlegende Paper kennenlernen.
Darum geht es inhaltlich:
In Proof Complexity, one tries to understand and analyze the computational resources required to prove or refute logical statements. More intuitively, one is interested in studying how to give short (and efficiently verifiable) proofs of the fact that a given CNF formula is unsatisfiable. The resolution calculus is one method how one can show unsatisfiability. This course will primarily focus on resolution as a proof system. Proof Complexity has not only a deep connection to the P vs. NP problem but also many exciting interrelations to the applied field of SAT Solving.
Eine Resolutionswiderlegung:
Voraussetzungen für die Teilnahme
Es bestehen im Prinzip keine inhaltliche Voraussetzungen für die Teilnahme an das Seminar. Die Studierenden sollten jedoch Eigenverantwortung und Eigeninitiative mitbringen und bereit sein, sich in ein neues Thema einzulesen.
Achtung:
Die Vergabe und Anmeldung zum Seminar erfolgt wie gewohnt zentral über Moodle: https://moodle.uni-ulm.de/course/view.php?id=27241.
Themenliste
Für die Teilnahme am Kurs ist es zwingend erforderlich sich im Moodle-Kurs anzumelden. Die vollständige Kommunikation, sowie Themen-Einteilung wird via Moodle erfolgen.
Eine vorläufige Themenliste:
- Allgemeine Beweissysteme.
- Baumartige Resolution.
- Exponentielle untere Schranke für die Resolution vom Schubfachprinzip.
- Kombinatorische Charakterisierungen von der Breite in der Resolution.
- Breite und Länge in der Resolution.
- Speicherbedarf für Resolutionwiderlegungen.
- Länge vs. Speicherplatz Trade-off Resultate.
- Resolutionstiefe.
- Das Cutting-Plane Beweissystem.
- Interpolation.
- Beweisysteme mit Symmetrieregeln.
- Resolution und SAT-Solving.
Eigene Themenvorschläge sind jederzeit willkommen!
Organisatorische Spielregeln
- Themengruppen mit maximal 2 Studierenden pro Grupe.
- Anwesenheit: maximal 2 mal fehlen wie bei ASQ.
- Vortragsdauer: 45-60 min pro Gruppe (Tafel oder Beamer).
- Ausarbeitung: 10-15 Seiten pro Gruppe (in LaTeX).
Sowohl Vortrag als auch Ausarbeitung darf wahlweise in Deutsch oder gerne auch auf Englisch gehalten werden.
Genaueres erklären wir in einer Vorbesprechung (siehe Moodle). Die Einteilung der Themen erfolgt ebenfalls über Moodle.