Proseminar (Algorithmen): Themenkomplex SAT-Solving
Inhalt
In diesem Proseminar wollen wir das SAT-Problem sowohl aus der theoretischen als auch praktischen (algortihmischen) Perspektive betrachten: SAT-Solver sind möglichst effiziente Algorithmen, die eine aussagenlogische Formel übergeben bekommen und untersuchen sollen, ob es eine erfüllende Belegung gibt. SAT ist jedoch NP-vollständig. Ob es also einen Algorithmus gibt, der SAT in Polynomialzeit löst, ist nicht bekannt (falls P ≠ NP ist, gibt es keinen solchen Algorithmus). Wir wollen in diesem Proseminar aber Möglichkeiten beleuchten, Algorithmen mit tolerabler Laufzeit (ohne P ≠ NP anzuzweifeln) für dieses Problem zu entwickeln. Grundlage für das Seminar werden ausgewählte Kapitel und Aspekte des Buches "The Satisfiability Problem: Algorithms and Analyses" von Uwe Schöning und Jacobo Torán sein.
Überblick über mögliche Seminarthemen
»Eine mögliche Auswahl an Themen mit kurzem Abstract und möglicher Literatur ist verlinkt.«
Organisatorisches
Zum Beginn des Seminars findet eine Vorbesprechung statt, an der Modalitäten des Proseminars besprochen werden und die einzelnen Themen an die Studierenden verteilt werden (siehe Randspalte rechts).
Die Vorträge (jeweils zu Zweit, Dauer ca. 45-60 min. pro gemeinsamen Vortrag*) finden wöchentlich statt, da die Themen teilweise aufeinander aufbauen (siehe Zeitplan unten). Zusätzlich zum Vortrag erfolgt eine gemeinsame Ausarbeitung (Umfang ca. 10-20 Seiten) in LaTeX.
* = Uns ist wichtiger, dass die Themen verständlich für die anderen Teilnehmer vorgetragen werden und die wichtigen Punkte im Vortrag abgedeckt sind. Daher erlauben wir ggfs. auch einen leicht längeren Vortrag, wenn das Kürzen auf Lasten des Verständnisses gehen würde.
Der Vortrag darf als Tafel-Vortrag oder mit Beamer gehalten werden (auch eine Kombination der Medien ist denkbar).
Sowohl Vortrag als auch Ausarbeitung dürfen wahlweise in Deutsch oder Englisch durchgeführt werden.
Bestehen des Proseminars
Uns ist wichtig, dass die Studierenden ein hohes Maß an Eigenverantwortung und Eigeninitiative mitbringen, sich in die teilweise neue Thematik einzuarbeiten, d.h. sich in die mathematischen Strukturen und Algorithmen einzuarbeiten und diese selbstständig erklären zu können.
Im Proseminar soll geschult werden:
- das Einarbeiten in ein wissenschaftliches Thema,
- das Verfassen einer wissenschaftlichen Arbeit über ein fest abgestecktes Thema,
- die Präsentation der wichtigsten Ergebnisse dieser kleinen "Forschungsarbeit" und das Halten eines wissenschaftlichen Vortrags.
Um das Proseminar erfolgreich zu bestehen erwarten wir daher:
- einen sehr gut vorbereiteten Vortrag (der am vereinbarten Zeitpunkt gehalten wird und rechtzeitig vorher mit dem Betreuer durchgesprochen wird),
- eine gute Ausarbeitung nach wissenschaftlichem Standard in LaTeX (die rechtzeitig abgegeben wird),
- die aktive Teilnahme an den Veranstaltungsterminen.
Wir verweisen auf Prof. Dr. Manfred Lehns Aufsatz "Wie halte ich einen Seminarvortrag?", der die Erwartungen an einen gelungenen Seminarvortrag sehr gut beschreibt.
Gruppenindividueller Zeitplan
Wir planen an, pro wöchentlichem Sitzungstermin eine Präsentation zu haben.
Roadmap:
Vorbesprechung: KW 42 (2018)
Erster Vortrag: KW 47 (2018); danach wöchentlich ein Gruppenvortrag
- Spätestens zwei Wochen vor individuellem Vortragstermin (den wir bei der Vorbesprechung festlegen werden) ist die vollständig ausgearbeitete Präsentation im Detail mit dem Betreuer durchzusprechen. (Ggfs. sind Mängel bis zum Vortragstermin zu korrigieren). Es ist zur Durchsprache der Vorträge rechtzeitig ein Termin zu vereinbaren. Nicht-Vereinbaren bzw. Nicht-Einhalten des Durchsprachetermines führt automatisch zum Nicht-Bestehen des Proseminars.
- Zwei Wochen nach individuellem Vortragstermin erwarten wir die Abgabe der Ausarbeitung. Eine verspätete Abgabe führt automatisch zum Nicht-Bestehen des Proseminars.
Bsp.: Vortrag in KW 47 -> Besprechung der Präsentation spätestens in KW 46; Abgabe der Ausarbeitung in KW 49.
Die Ausarbeit wird dann von uns korrigiert. Dies macht es ggfs. nötig, die Ausarbeitung zu korrigieren und Mängel zu beheben.
Bitte nutzen Sie die wöchentlichen Termine oder Sprechzeiten der Betreuer, um Fragen zu stellen. Wir erwarten einen fristgerecht gehaltenen und durchgesprochenen Vortrag. Fragen sollten und dürfen Sie gerne rechtzeitig vorher besprechen.
Voraussichtliche Vortragstermine:
Kalenderwoche | Themen | Vortragende |
KW 47 (2018) | Das SAT-Problem | Klassen, Schmid |
KW 48 (2018) | Erfüllbarkeit durch Kombinatorik und das Lovász Local Lemma | Bevap, Koper |
KW 49 (2018) | Polynomial-lösbare Spezialfälle von SAT | Krug, Wilhelm |
KW 50 (2018) | DPLL-artige Algorithmen I: Monien-Speckenmeyer | Mitterbauer, Schäufele |
KW 51 (2018) | DPLL-artige Algorithmen II: Paturi-Pudlák-Zane & CDCL | Bachhofer, Eskin |
Weihnachtsferien | ||
KW 02 (2019) | Local Search I: Restarts und Covering Codes | Burr, Ott |
KW 03 (2019) | Local Search II: WalkSAT und der Moser-Scheder-Algorithmus | Dardouri, Rahal |
KW 04 (2019) | Divide-and-Conquer für 3-SAT und Stålmarks Algorithmus | Fandrich, Jutz |
KW 05 (2019) | Resolution und das Pigeon Hole Principle | noch zu vergeben |
Empfohlene Voraussetzungen für das Proseminar
- Grundkenntnisse der Informatik z. B. aus Formale Grundlagen oder Algorithmen und Datenstrukturen: z. B. Landausche O-Notation, etc.
- Grundlegende Mathematik, z. B. aus Analysis 1 für Informatiker und Ingenieure: Binomialkoeffizienten, Exponentialfunktionen, Logarithmen, etc.
- Die Bereitschaft sich fehlende Konzepte aus der Mathematik und Informatik selbstständig anzueignen. Teilweise brauchen wir z. B. etwas Grundlagenwissen über Wahrscheinlichkeitstheorie (Begriffe Wahrscheinlichkeit eines Ereignisses, Gegenereignis, Erwartungswert, Markov-Ungleichung, Jensen-Ungleichung, etc.).
LaTeX-Vorlagen
Wir erwarten verpflichtend eine Ausarbeitung, die mit LaTeX erstellt wurde. Dies soll Ihnen später beim Erstellen Ihrer Bachelorarbeit zu gute kommen.
Bitte planen Sie genug Zeit für eine Einarbeitung in LaTeX ein.
Um Sie zu unterstützen, haben wir folgende Dokumente erstellt:
- Vorlage für die Ausarbeitung (Stand 2018)
- Vorlage für die Präsentation (Stand 2018). Nota bene: Auch ein Tafelvortrag ist erlaubt!
LaTeX-Programme:
Termin für Vorträge
Die Vorträge finden jeweils freitags von 16:00 (sine tempore!) bis ca. 18:00 Uhr in O27/531 statt.
Vorbesprechung
Einführungsveranstaltung in der ersten Semesterwoche am Freitag, den 19.10. um 17:00 Uhr in O27/531.
Bitte erscheinen Sie vollzählig zur Vorbesprechung, da dort wichtige organisatorische Details besprochen und die Vorträge verteilt werden. Bitte informieren Sie sich vorab über die Vortragsthemen!
Hier finden Sie die Folien der Vorbesprechung.