Algorithmen der Logik

Aktuelles

  • Einführungsveranstaltung
    28.10.2014 - 16:00 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 oder falsch.

 

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 CDCL SAT Solver (ein Algorithmus, der mittels theoriegetriebener Suche das Wortproblem entscheidet) implementiert werden.

 

Bei Interesse können sich die Studenten unverbindlich bei Oliver Gableske melden (oliver.gableske(at)uni-ulm.de).

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, Leistungsnachweise

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

Dieses Projekt richtet sich an Master Studenten der Informatik und weiteren Studiengaengen, die mit der Informatik verwandt sind (z.b. Mathematik oder Physik).

Ein Student, der das Projekt erfolgreich abschliesst, bekommt 10LP im Rahmen des Algorithm Engineering Projektmoduls der Theoretischen Informatik. Um das Projektmodul abzuschliessen ist mindestens eine Vorlesung, die mit diesem Projektmodul verknuepft werden kann, erforderlich (bspw. SAT Solving bei Prof. Dr. Schoening).

Der Leistungsnachweis fuer das gesamte Projektmodul Algorithm Engineering wird durch eine muendliche Pruefung bestimmt. Die muendliche Pruefung bezieht sich jedoch nur auf den Stoff der gewaehlten Vorlesung (also bspw. SAT Solving).

Die Gesamtnote dieser muendlichen Pruefung ergibts ich aus der Note zum Projekt (10LP) sowie der muendlichen Pruefung der Vorlesung (bspw. 6LP bei SAT Solving).

Sonstiges

Sollten sich zum Ende des Semesters genügend lauffähige Algorithmen gefunden haben, bei denen die Studenten einen Vergleich wünschen, wird es einen Wettbewerb (gerechnet auf dem BW Uni Cluster in Karlsruhe) geben, bei dem es verschiedene Preise in verschiedenen Kategorien zu gewinnen gibt. Vergleiche hierzu auch www.satcompetition.org.

Stichworte

Aussagenlogik, Quantorenlogik, Prädikatenlogik, SAT, QBF, CSP

Verantwortlich

Dipl.-Inf. Oliver Gableske
Prof. Dr. Uwe Schöning

Weitere Informationen

Per email: oliver.gableske(at)uni-ulm.de
Per LSF: LSF-Eintrag

Termine

Montag, den 28.04.2014 - 16:00 c.t.
Einführungsveranstaltung

Dienstag, den 06.05.2014 - 16:00 c.t.
Theorierunde 1