Aktuelles

• Grundlagen 2 - SAT Solver und deren praktische Anwendbarkeit09.05.2012 (Mittwoch), 14:00 c.t.
  Raum o27/531
  Thama sind SAT Solver Paradigmen und einige Anwendungsbeispiele für SAT Solver. Weiterhin werden einige organisatorische Dinge festgelegt.
  
• Grundlagen - Logiken, Kalküle, Entscheidungsprobleme
  02.05.2012 (Mittwoch), 14:00 c.t.
  Raum o27/531.
  Thema sind Syntax und Semantik von Aussagenlogik, Quantifizierten Boole'schen Formeln und Prädikatenlogik. Weiterhin beschäftigen wir uns mit dem Resolutionskalkül (sowohl für Aussagenlogik als auch Prädikatenlogik). Es werden diverse Sprachen wie SAT und TQBF sowie die dazugehörigen Wortprobleme eingeführt.
• Einführungsveranstaltung
  18.04.2012 (Mittwoch), 14:00 Uhr c.t. und
  25.04.2012 (Mittwoch), 14:00 Uhr c.t.
  Raum o27/531 (Seminarraum des Instituts für Theoretischen Informatik). Die Einführungsveranstaltung ist unverbindlich.

Projektinformationen

Zusammenfassung

In diesem Projekt geht es vorrangig um das Kennenlernen von Logiken und Algorithmen, die mit diesen Logiken umgehen. Dabei sollen neben den theoretischen Grundlagen auch praktische Erkenntnisse über den Umgang mit Logiken und deren Einsatzzweck vermittelt werden.

Inhalt

Ein prominentes Beispiel für eine Logik ist die Aussagenlogik welche keine Quantoren, keine Prädikate und keine Funktionen kennt; lediglich binäre Variablen und oft nur die logischen Konnektoren "Und", "Oder" und "Nicht" finden bei dieser Logik Verwendung. Die binären Variablen dieser Formeln beschreiben elementare Ereignisse die entweder gegeben sind (=1), oder nicht (=0). Eine aussagenlogische Formel wird dann mit Hilfe dieser Gegebenheiten (auch Belegung genannt) ausgewertet und evaluiert entweder auf wahr (=1) oder falsch (=0).

Oft hat man lediglich die Formel gegeben (also die Bedingungen hinter einer Aussage, die man machen will), und keinerlei Gegebenheiten (man weiß also nicht, was zutreffen muss und was nicht damit alle Bedingungen erfüllt sind). Die Frage, die sich dann oft stellt ist: Gibt es überhaupt irgendeine Belegung, die die Formel wahr macht? Mit Hilfe der Algorithmen die solche Fragestellungen beantworten, ist es bspw. möglich das Wortproblem von Sprachen wie SAT (die Menge aller erfüllbaren aussagenlogischen Formeln) zu lösen.

Einerseits ist SAT ein kanonisches Bispiel für eine Sprache bei der das Wortproblem (Ist die gegebene Formel erfüllbar?) schwierig zu lösen ist (SAT ist NP-vollständig). Aus theoretischer Sicht macht es also wenig Sinn ein Problem, welches man lösen muss, nach SAT zu reduzieren. Andererseits kann man alle NP-Probleme nach SAT reduzieren, was einen Algorithmus, der das Wortproblem für SAT tatsächlich löst, vielfältig einsetzbar macht. Prinzipiell kann ein solcher Alorithmus alle Probleme aus NP lösen und eignet sich damit als generischer Problemlösungsalgorithmus für viele praktische Probleme.

In der Praxis werden solche Algorithmen (bezogen auf SAT als SAT Solver bezeichnet) vermehrt eingesetzt. Bekannte Fahrzeughersteller wie Daimler-Benz, VW, Audi u.v.a. verwenden sie um die Kundenkonfigurationen von Fahrzeugen zu prüfen. Dies bedeutet insbesondere, dass der Kunde einen Wunsch hinsichtlich der Ausstattung seines Fahrzeuges nennen kann (wofür es prinzipiell extrem viele Möglichkeiten gibt). Damit gibt der Kunde die Gegebenheiten für ein Fahrzeug vor. Der Fahrzeughersteller prüft nun mittels SAT Solver, ob die Gegebenheiten einen Widerspruch erzeugen (also die Formel, die die Faktenbasis für alle gültigen Fahrzeugkonfigurationen bildet, wird unerfüllbar und ist nicht mehr in SAT), oder ob die Formel widerspruchsfrei bleibt. Im letzteren Fall kann das vom Kunden speziell konfigurierte Auto auch tatsächlich gebaut werden.

Auch komplexere Logiken, wie die Quantorenlogik (mit dem Wortproblem OBF; Ist die Formel gültig?) sowie die Prädikatenlogik erster Stufe sollen betrachtet werden, um ein theoretischen Verständnis von Logiken zu vermitteln.

Der praktische Anteil des Projekts befasst sich mit der Implementierung von Algorithmen, die sich mit Aussagenlogik beschäftigen. Hier sollen ein Preprozessor (also ein effizient laufender Algorithmus, der eine aussagenlogische Formel lediglich vereinfacht) und ein SAT Solver (ein Algorithmus, der mittels Suche das Wortproblem entscheidet) implementiert werden.

Bei Interesse können sich die Studenten unverbindlich bei Oliver Gableske melden (oliver.gableske(at)uni-ulm.de). Ein erster Besprechungstermin wird noch bekannt gegeben.

Benötigte Vorkenntnisse

Vorausgesetzt wird ein grundlegendes Verständnis der Aussagenlogik, welche Diplom/Master Studenten durch ihr Grund- bzw. Bachelorstudium bereits erlangt haben sollten. 

Zudem sind Kenntnisse in einer gängigen Programmiersprache wie C, C++ oder Java von Vorteil.

Projektziele, Leistungspunkte, Scheine

Ziel des Projekts ist das entwerfen und implementieren eines SAT Preprozessors sowie eines SAT Solvers. Beide Programme sollen in einer Abschlussarbeit von ca. 12 Seiten beschrieben, und in einem Abschlussvortrag von ca. 30 Minuten vorgestellt werden.

Jeder Student, der dieses Projekt erfolgreich beendet, bekommt einen Schein also Leistungsnachweis ausgestellt (auf Wunsch können wir diese auch mit einer Note versehen).

Die Zahl der Leistungspunkte für dieses Projekt hängt von der Studienart der Studenten ab. Master-Studenten erhalten 10 LP, Diplom-Studenten erhalten 8LP.

Sonstiges