Forschungsgruppe veranstaltet internationalen SAT-Wettbewerb

Prämiert wurden die besten Programme zur Lösung aussagenlogischer Probleme

Alle zwei Jahre messen sich die besten Programmierer beim internationalen Wettbewerb »SAT-Race«, der in diesem Jahr von einer Forschungsgruppe des Instituts für Theoretische Informatik veranstaltet wurde.

Ausgezeichnet werden die besten »SAT-Solver«, d.h. die besten Programme zur Lösung des aussagenlogischen Erfüllbarkeitsproblems (SAT-Problem). Dabei handelt es sich um ein algorithmisches Problem, das für die Informatik von zentraler Bedeutung ist. Das SAT-Problem fragt für eine gegebene aussagenlogische Formel (z.B. "wenn X, dann Y"), ob diese eine Lösung besitzt, d.h. ob es eine Möglichkeit gibt, durch geschickte Wahl der Eingabevariablen die gesamte Formel wahr zu machen.

"Die Fortschritte, die im SAT-Solving in den letzten Jahren erzielt wurden, sind enorm. Heute können in bestimmten Anwendungsgebieten selbst Probleme mit Hunderttausenden von Variablen zuverlässig gelöst werden", so Carsten Sinz, Leiter der Forschungsgruppe "Verifikation trifft Algorithmik" und Veranstalter des SAT-Race.

Die SAT-Solver müssen im Wettbewerb 100 anwendungsnahe Probleme aus den Bereichen Hardware-Verifikation, Software-Verifikation, Crypto-Analyse, Diagnose und Bio-Informatik lösen. Dabei stehen jedem Programm maximal 15 Minuten zur Lösung eines Problems zur Verfügung.

Von den 32 eingereichten SAT-Solvern aus neun Nationen qualifizierten sich insgesamt 26  zur Teilnahme am SAT-Race 2010. Als beste Programme in drei Kategorien wurden die in Frankreich, Österreich und Schweden programmierten SAT-Solver CryptoMiniSat, plingeling und MiniSAT++, ausgezeichnet. Die gesamte Rangliste kann auf der Veranstaltungswebsite eingesehen werden.

Die Gewinner des SAT-Race 2010 wurden im Rahmen der 13th International Conference on Theory and Applications of Satisfiability Testing bekannt gegeben, die vom 11.-14. Juli in Edinburgh stattfand.

Tweet