Ulmer Informatiker haben für eines der schwierigsten Probleme ihres Fachs den derzeit besten Algorithmus gefunden. Bei der internationalen SAT-Competition im nordamerikanischen Ann Arbor löste „Sparrow 2011“ das Erfüllbarkeitsproblem der Boole‘schen Logik in zwei Kategorien am effizientesten. Somit konnten sich Adrian Balint und Andreas Fröhlich, beide vom Ulmer Institut für Theoretische Informatik, und ihre kanadischen Kollegen gegen Mitbewerber aus 30 Nationen durchsetzen – darunter Computerexperten von IBM und Microsoft.
Zudem gewann der Ulmer Promotionsstudent Oliver Gableske mit seinem Algorithmus „EagleUp“ eine Bronzemedaille. Auch bei der parallel stattfindenden MaxSATCompetition war das Ulmer Institut für Theoretische Informatik erfolgreich: Doktorand Adrian Kügel sicherte sich mit dem Algorithmus „AKMaxSAT“ gleich sechs erste Plätze in verschiedenen Kategorien. Die SAT-Competition fand Ende Juni, im Rahmen der SAT 2011-Konferenz statt – der vielleicht wichtigste Tagung auf diesem Gebiet der Informatik.
Bei der Lösung des SAT-Problems wird entschieden, ob eine Formel der Aussagelogik erfüllbar ist. Dabei können Variablen der Formel lediglich die Werte Null oder Eins annehmen. Außerdem sind nur drei logische Operatoren möglich. „In der Informatik lassen sich alle komplexen Probleme auf ein SAT-Problem reduzieren“, erklärt Promovend Adrian Balint. Während sich das SAT-Problem prinzipiell lösen lässt, kann bei einem MaxSAT-Problem lediglich eine Belegung mit der kleinsten Anzahl unerfüllter Klauseln erreicht werden.
Die Anwendungsbereiche sind übrigens vielfältig und reichen von der Verifikation logischer Schaltkreise bis zur Überprüfung von Computerprogrammen.
Der Ulmer Algorithmus Sparrow 2011 wird Standards für die kommenden Jahre setzten. „Dabei ist unser Algorithmus recht einfach, schlank und elegant – wie ein Spatz eben“, erklärt Balint. Sparrow 2011 basiere auf einem Vorgänger-Algorithmus. Zusätzlich hätten sie etwa sechs Monate Arbeit investiert und den „Spatzen“ unter anderem auf dem Baden-Württembergischen Supercomputer bwGRiD getestet.
In Ann Arbor sind zunächst alle eingesandten Algorithmen über zwei Monate auf 400 parallel arbeitenden Rechnern getestet worden. Die Kriterien: Nach möglichst kurzer Rechenzeit mussten sie bei SAT-Eingaben korrekte Ergebnisse liefern. Lediglich 60 Einsendungen haben es in die Endrunde geschafft und sind von einer Jury aus internationalen Experten analysiert worden. Letztendlich durften die Ulmer in vielen Kategorien jubeln. Auf ihren Lorbeeren ausruhen wollen sich Adrian Balint und seine Kollegen allerdings nicht: „Bis zur nächsten SAT-Competition dauert es noch zwei Jahre, wir entwickeln aber ständig etwas Neues“, sagt Balint. Aktuell denke man darüber nach, den nächsten internationalen SAT-Wettbewerb in Ulm zu organisieren.
Von Annika Bingmann