Perlen der Informatik Sommersemester 2014

Vorlesungsinhalt:

Die Vorlesung basiert auf dem Buch

• Uwe Schöning, Jacobo Torán Das Erfüllbarkeitsproblem SAT, Lehmanns Media, 2012

"SAT (für satisfiability) ist der Name des bekanntesten NP-vollständigen Problems, des Erfüllbarkeitsproblems der Aussagenlogik. Gegeben ist hierbei eine Formel mit Boole'schen Variablen und Verknüpfungen und gesucht wird eine Lösung , also eine Wertezuweisung an die Variablen, so dass die Formel wahr wird. Dieses algorithmische Problem ist Dreh- und Angelpunkt für alle NP-Vollständigkeitsnachweise und wurde schon als Drosophila der Algorithmik bezeichnet. Für SAT werden seit einiger Zeit leistungsstarke Algorithmen entwickelt, die in der Lage sind, Formeln mit hunderten oder tausenden von Variablen zu lösen. Bei schwierigen Formeln mit nur wenigen Lösungen kommt dies der sprichwörtlichen Suche nach der Nadel im Heuhaufen gleich. Wie derartige Algorithmen arbeiten und wie die zugehörigen logischen Kalküle und heuristischen Suchmethoden eingesetzt werden, wird in diesem Buch die erste deutschsprachige Veröffentlichung zum Thema eingehend und fundiert erklärt."

SAT wurde schon in der Vorlesung "Diskrete Strukturen" eingeführt. Die dort präsentierten Inhalte werden hier erweitert und vertieft. In den Übungen zu "Diskrete Strukturen" wurde auch angedeutet, wie man Public-Domain Software für SAT anwenden kann. Die Vorlesung richtet sich an Studierenden, die einerseits Freude an theoretischen Inhalten haben, aber gleichzeitig Interesse und Neugier für den Umgang mit SAT-Solvern mitbringen.

In der Vorlesung wird zunächst erklärt, warum SAT ein so bedeutendes Problem ist. Es wird gezeigt, dass viele andere Entscheidungsprobleme (Graphenprobleme wie Färbbarkeit von Graphen und Existenz von Hamiltonkreisen, Entscheidungsversionen von Optimierungsproblemen wie Knapsack oder Bin-Packing, logische Puzzeln wie Sudoku oder das Damenproblem, Probleme der Zuverlässigkeitsnalayse wie Äquivalenz von Schaltkreisen oder Ausfürbarkeit von Anweisungssequenzen) auf SAT reduziert werden kann. Die Reduktionen können dann von den Teilnehmern mit Hilfe von SAT-Solvern implementiert und getestet werden. Die Theorie der NP-Vollstädigkeit und ihre Bedeutung werden auch kurz eingeführt. Wie es dann weitergeht wird (zum Teil) von den Teilnehmern bestimmt.

Die Vorlesung hat einen anderen Stil als "Diskrete Strukturen". Es wird direkter zu den Kernfragen gegangen. Der Spassfaktor oder die mathematische Schönheit eines Ergebnisses haben mehr Einfluss auf die Inhalte.