Home | deutsch  | Legals | Sitemap | KIT

Seminar SAT-Solving

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