Homepage: Effiziente Lösung

Der Doktorand Benjamin Kaufmann vom Institut für Informatik der Universität Potsdam hat mit seinem Programm „clasp“ beim Internationalen Wettbewerb für SAT-Solver zwei erste Plätze belegt. Wie die Uni mitteilte, habe er sich damit erfolgreich gegen 50 Mitbewerber durchgesetzt. Der Wettbewerb wurde im Rahmen der SAT-Konferenz 2009 in Swansea (Großbritannien) ausgetragen.

SAT bedeutet aussagenlogische Erfüllbarkeit (engl. Satisfiability) und ist ein kombinatorisches Suchproblem, das viele praktisch relevante Fragestellungen betreffen kann. Populäre Anwendungen finden sich in der Bio-Informatik, in der Hardware- und Softwarekonfiguration und in der Kryptographie. Die Programme, sogenannte SAT-Solver, versuchen, das Problem so effizient wie möglich zu lösen. Das Programm „clasp“ verbinde erstmals Wissensrepräsentation und Wissensverarbeitung effektiv in einem System miteinander. PNN