Projektschreibung

Das Projekt SATRIX beschäftigt sich mit dem Erfüllbarkeitsproblem – oder kurz SAT von engl. satisfiability. Es soll der gesamte Ablauf von der Modellierung einer Fragestellung als SAT-Problem bis hin zur effizienten Lösung einer gegebenen Instanz betrachtet werden. Insbesondere sollen Fragestellungen aus dem Schaltkreisentwurf untersucht werden.

In eigener Sache

Das Projekt Satrix hat sich mit einem ziemlich öde klingenden, aber dennoch sehr wichtigem Problem der Informatik beschäftigt: Der Erfüllbarkeit.

Oder:
Wie bekomme ich möglichst schnell eine gültige Belegung für eine boolesche Formel. Die letzten zwei Jahre haben wir uns also darüber das Hirn zermattert, wie man schneller herraus finden kann, dass zum Beispiel x=1 und y=0 die Formel f = x AND ~y erfüllt.

Warum das Ganze? Ganz einfach: Eine ganze Menge echter Probleme lassen sich auf das Erfüllbarkeitsproblem (übrigens auch bekannt als SAT-Problem) abbilden. Findet man also schnelle Algorithmen für SAT hat man gleichzeitig auch schnelle Algorithmen für zig andere Probleme: Graphenfärben, Schaltkreisverifikation, optimale Stundenplanbelegung, beste Spielstrategie für 'Vier gewinnt' und, und, und (nur Wettervorhersagen klappen noch ned so gut).

Wirklich toll also, dieses SAT. Nur gibt es ein Problem dabei: SAT gehört mit zu der Klasse der NP-Probleme. Das heißt, die sind gaaaaaaaanz dolle schwer.

Naja, fast. Eigentlich sind sie nur schwer, wenn man blöderweise immer die falsche Belegung rät. Aber genau das ist das Hauptproblem.

Also haben wir mal geschaut, was man an den bisher bekannten Lösungsstrategien verbessern kann - wie man also weniger blödsinnige Entscheidungen trifft oder aus denen besser lernen kann. Und herraus kamen eine ganze Reihe an Ideen, wie man SAT an sich, Graphenfärben und auch Verifkation von Schaltkreisentwürfen schneller lösen kann. Es lohnt sich, sich die mal anzuschauen!

Das alles klingt für dich jetzt zu langweilig, zu theoretisch und überhaupt viel zu formellastig? Lass' dich davon nicht abschrecken. Wenn Suduko eine halbe Nation in's Tüftelfieber versetzen kann, dann kann das SAT schon lange. Also schau ruhig mal bei uns vorbei!

Betreuung
Dipl. Inf. Görschwin Fey
Dipl. Inf. Daniel Grosse

Leitung
Prof. Dr. Rolf Drechsler

Homepage des Projektes
leider keine angegeben