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,
  • eine gute Ausarbeitung nach wissenschaftlichem Standard in LaTeX,
  • 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

  • Zwei bis spätestens eine Woche 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).
  • Zwei Wochen nach individuellem Vortragstermin erwarten wir die Abgabe der Ausarbeitung.

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 Vortrag. Fragen sollten und dürfen Sie gerne rechtzeitig vorher besprechen.

Voraussichtliche Vortragstermine:

KalenderwocheThemen
KW 47 (2018)Das SAT-Problem 
KW 48 (2018)Erfüllbarkeit durch Kombinatorik und das Lovász Local Lemma
KW 49 (2018)Polynomial-lösbare Spezialfälle von SAT
KW 50 (2018)
DPLL-artige Algorithmen I: Monien-Speckenmeyer
KW 51 (2018)DPLL-artige Algorithmen II: Paturi-Pudlák-Zane & CDCL
Weihnachtsferien
KW 02 (2019)Local Search I: Restarts und Covering Codes
KW 03 (2019)
Local Search II: WalkSAT und der Moser-Scheder-Algorithmus
KW 04 (2019)Divide-and-Conquer für 3-SAT und Stålmarks Algorithmus
KW 05 (2019)

Resolution und das Pigeon Hole Principle

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:

  1. Vorlage für die Ausarbeitung (Stand 2018) 
  2. Vorlage für die Präsentation (Stand 2018). Nota bene: Auch ein Tafelvortrag ist erlaubt!

LaTeX-Programme:

  1. Distribution für Windows, Mac oder Linux (MiKTeX)
  2. LaTeX-Editor für Windows, Mac oder Linux (TeXstudio)

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.