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).