Seminar SAT-Solving
- type: seminar
- semester: Hauptdiplom
- place: seminar room -107
-
time:
Mon. 15:45-17:15
- start: 14.04.
-
lecturer:
C. Sinz, H. Post
- sws: 2
- lv-no.: 24827
-
information:
Das Seminar wurde zusammengelegt mit dem Seminar "Formale Software-Entwicklung" von Prof. Schmitt.
Das aussagenlogische Erfüllbarkeitsproblem (SAT-Problem) spielt in Theorie und Praxis eine herausragende Rolle. Es ist das erste als NP-vollständig erkannte Problem, und auch heute noch Ausgangspunkt vieler komplexitätstheoretischer
Untersuchungen. Darüber hinaus hat sich SAT-Solving inzwischen als eines der wichtigsten grundlegenden Verfahren in der Verifikation von Hard- und Software
etabliert.
Im Seminar wollen wir historische und aktuelle Artikel rund um das SAT-Problem
betrachten zu Themen wie:
• Datenstrukturen und Algorithmen zum SAT-Solving
• Komplexität, handhabbare Unterklassen (tree-width, FPT)
• Effiziente Codierung kombinatorischer Probleme
• Visualisierung der Struktur von SAT-Problemen
• Querbeziehungen zur statistischen Physik
• Bounded Model Checking
• SAT-Solving in der Produkt-Konfiguration
• Software-Verifikation mittels SAT-Solvern
• SMT (Satisfiability Modulo Theory)
Organisatorisches
- Vorträge können auf Englisch oder Deutsch gehalten werden.
- Folien spätestens zwei Wochen vor Vortragstermin mit dem Betreuer durchsprechen.
- Ausarbeitung: 10-15 Seiten, Abgabe zum Ende des Semesters
- Vortragsdauer max. 40 Minuten plus 10 Minuten für Diskussion
- Tipps zu Vortrag und Ausarbeitung: Seminarleitfaden von K. und N. Weicker
- Vorträge am 09.07. finden im Seminarraum -109 statt.
Termine
14.04.2008: Vorbesprechung
05.05.2008: Einführung SAT-Solving (C. Sinz)
09.07.2008: Vorträge (max. 45min + 5min Diskussion)
14:00 Markus Iser: Visualisierung der Struktur von SAT-Instanzen mittels Graph-Layout
14:50 Simon Roth: Software Verifikation: Abstraction Refinement
15:40 Jan Rochel: Tree Decomposition für SAT