Adrian Balint und Andreas Fröhlich vom Ulmer Institut für Theoretische Informatik und ihre kanadischen Kollegen konnten sich somit gegen Mitbewerber aus 30 Nationen durchsetzen – unter ihnen auch 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.
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.
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.
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.
