Informationen zum Seminar
"SAT-Engines" (WS 2000/2001)
Veranstalter Prof. Dr. Bernd Becker
Priv.-Doz. Dr. Rolf Drechsler
Mitwirkende Dipl.-Inform. Wolfgang Günther
Beschreibung In vielen Bereichen der Informatik werden SAT Engines verwendet, um die Erfüllbarkeit ("Satisfiability") von in konjunktiver Normalform gegebenen Formeln zu bestimmen. Unter anderem seien hier Anwendungen aus dem automatisierten Schaltkreisentwurf genannt, wie die Verifikation ("Berechnen zwei Schaltungen die gleiche Funktion?") oder die Testbarkeit ("Ist ein Fehler eines bestimmten Gatters an den Ausgängen feststellbar?"). Jedoch auch in der künstlichen Intelligenz werden SAT Engines häufig verwendet.

SAT ist ein klassisches NP-vollständiges Problem und ist im allgemeinen nicht effizient lösbar. Dennoch gibt es Verfahren, die in vielen praktischen Anwendungen gute Ergebnisse zeigen. Vor allem in den letzten 10 Jahren wurden neue Techniken entwickelt, die ein effizientes Lösen von Formeln mit über 1000 Variablen ermöglichen.

Im Gegensatz zu Binary Decision Diagrams (BDDs), die alle möglichen Lösungen berechnen, geht es beim Sat Engines vor allem darum, eine L"osung anzugeben, falls es eine gibt. In vielen Anwendungen reicht die Kenntnis einer Lösung aus. Dadurch kann man auf eine aufwendige Repräsentation der gesamten Funktionalität verzichten. Auf der anderen Seite bieten BDDs die Möglichkeit, die dargestellte Funktion automatisiert und effizient zu reduzieren, was bei SAT-Algorithmen so bisher noch nicht bekannt ist. Es gibt bisher kein Verfahren, das die Vorteile beider Methoden vereint.

In diesem Seminar sollen sowohl einführende Vorträge über die Basisalgorithmen als auch Originalarbeiten aus vorderster Front der Forschung vorgestellt und diskutiert werden. Insbesondere wird auf die Möglichkeiten bei der Verifikation von Schaltungen eingegangen. Ziel ist es, den Teilnehmern einen Überblick der zur Zeit existierenden Lösungsansätze und Anwendungen zu ermöglichen.

Interessierten Teilnehmern kann eine begleitende oder an das Seminar anschließende Studien- oder Diplomarbeit angeboten werden. 
Insbesondere gibt es auch Kooperationsmöglichkeiten mit der Industrie. Als Ergänzung eignet sich insbesondere die Vorlesung Graphbasierte Funktionsdarstellung.

Das Seminar wird in mehreren Blöcken stattfinden, die auf das Wintersemester verteilt sind. Die Vorbesprechung ist zu Beginn des
Wintersemesters. Anmeldungen werden gerne auch vorher von Wolfgang Günther entgegengenommen (Raum 051-01-030).

Zeit und Ort 2-stündige Blockveranstaltung nach Vereinbarung
im SR 00-034, Geb. 051