Als „größte wissenschaftliche Veranstaltung in der Geschichte der Logik“ wurde die Konferenz „Vienna Summer of Logic“ mit immerhin 2000 Teilnehmern von der TU Wien beworben. Umso höher ist es Professor Uwe Schöning, Leiter des Ulmer Instituts für Theoretische Informatik, und seinen Mitarbeitern Oliver Gableske sowie Dr. Adrian Balint (ehemals Uni Ulm) anzurechnen, dass sie bei den „Olympischen Spielen der Logik“ gleich zwei Medaillen abgeräumt haben. Bei dieser Olympiade, die Mitte Juli im Zuge der Konferenz ausgerichtet wurde, ging es natürlich nicht um Stabhochsprung oder Synchronschwimmen. Vielmehr hat die TU Wien einen „Wettlauf der Computerprogramme“ ausgerichtet.
Bei einem Vorlauf an der University of Texas (USA) hatten sich insgesamt 70 Programme für den tatsächlichen Wettbewerb („SAT-Competition“) in Wien qualifiziert: In einer vorgegebenen Zeit mussten die so genannten SAT-Solver dann möglichst viele Probleme aus den unterschiedlichsten Bereichen lösen – dabei ging es zum Beispiel um die Verifikation von Schaltkreisen. Der Ulmer Doktorand Oliver Gableske erklärt den Ansatz der SAT-Competition: „Zunächst wird ein Problem in eine aussagelogische Formel überführt. Dann folgt der Erfüllbarkeitstest: Mit einem SAT-Solver wird entschieden, ob die aussagelogische Formel eine Lösung hat – was wiederum Rückschlüsse auf die Lösung des Originalproblems zulässt.“ Eigentlich hätten die Urheber gar nicht zum „Summer of Logic“ nach Wien reisen müssen: Die SAT-Solver arbeiteten völlig ohne ihr Zutun.
Die „Olympischen Spiele der Logik“ verliefen für das Team Schöning/Balint und Oliver Gableske hocherfolgreich: In einem Problembereich war Gableskes sequentieller SAT-Solver, der zufällig erzeugte Probleme mit nur einem Prozessorkern löst, sogar so schnell, dass er parallele SAT-Solver besiegt hätte. Diese Solver greifen auf immerhin zwölf Prozessorkerne zurück.
Die Informatiker nutzten die Konferenz in Wien weiterhin für den Austausch mit Kollegen. „Ich habe viele Ideen für meine Arbeit mitgenommen und sogar Anwender meiner Software getroffen“, resümiert Oliver Gableske.
Auf den Kurt Gödel-Medaillen der Ulmer prangt übrigens das Konterfei des namensgebenden Wiener Logikers. Die Auszeichnungen wurden natürlich bei einer „olympischen Siegerehrung“ verliehen.
