Hochrangige Auszeichnungen für Dissertation

Dominik Schreiber bei der Verleihung des Fahiem-Bacchus Awards (links) sowie der Übergabe des GI-Dissertationspreises (rechts)

Die am Lehrstuhl Algorithm Engineering der KIT-Fakultät für Informatik entstandene Dissertation behandelt parallele und verteilte Lösungsansätze für das Problem der aussagenlogischen Erfüllbarkeit (engl. satisfiability, kurz SAT). Dabei geht es darum, für eine gegebene logische Problemstellung eine konsistente Lösung zu finden oder zu erkennen, dass keine solche Lösung existiert. SAT-Solver finden in zahlreichen Disziplinen praktische Anwendung, etwa zur systematischen Analyse wichtiger Hardware- und Software-Komponenten in Bezug auf ihre Korrektheit und Sicherheit. Die massiv parallelen Ansätze aus Dominik Schreibers Dissertation haben sich als der Stand der Technik für skalierbares SAT-Solving etabliert und dominieren seit 2020 die entsprechenden ("Cloud"-) Kategorien einschlägiger internationaler Wettbewerbe. "Die Revolution durch neuronale Netze wird entscheidend von der Nutzung paralleler Hardware vorangetrieben. Dominik Schreibers Arbeit geht für symbolische künstliche Intelligenz einen wichtigen Schritt in diese Richtung, erklärt Schreibers Doktorvater Professor Peter Sanders, Informatikprofessor am Karlsruher Institut für Technologie.

Mit dem Dissertationspreis der Gesellschaft für Informatik (GI) werden jährlich 1-3 Dissertationen aus der Informatik ausgezeichnet, die im deutschsprachigen Raum entstanden sind – der Preis wird gemeinsam mit der Österreichischen Computergesellschaft (OCG) und der Schweizer Informatik Gesellschaft (SI) verliehen. Dominik Schreiber erhält den diesjährigen Dissertationspreis gemeinsam mit Prof. Mennatallah El-Assady (ETH Zürich). Die Verleihung fand am 25. September im Rahmen des INFORMATIK24-Festivals in Wiesbaden statt.
Die Präsidentin der GI, Christine Regitz, kommentiert: „Dr. Schreibers Dissertation zeigt eindrucksvoll, wie theoretische Informatik praxisrelevante Probleme lösen kann. Seine Forschung liefert nicht nur neue algorithmische Ansätze, sondern auch hochskalierbare Implementierungen, die in der Praxis signifikante Verbesserungen erzielen.“

Außerdem hat Dominik Schreiber  für seine Dissertation „Scalable SATSolving and its Application“ den neu gestifteten Fahiem-Bacchus Award erhalten. Der Fahiem Bacchus Award zeichnet auf internationaler Ebene eine Dissertation aus den Jahren 2022-2023 im Bereich der aussagenlogischen Erfüllbarkeit und verwandten Themenbereichen aus. Er wurde am 24. August auf der International Conference on Theory and Applications of Satisfiability Testing in Pune (Indien) verliehen. Die Auszeichnung ist nach Fahiem Bacchus (1957-2022) benannt, der die Forschung zu aussagenlogischer Erfüllbarkeit und automatisiertem Schlussfolgern maßgeblich vorangetrieben hat. "This outstanding thesis presents the state-of-the-art of parallelizing the most important NP-hard problem, i.e., propositional SAT solving. [...] The thesis work already produced exceptional impact in a highly visible field both on the academic as well as industrial side”, so Professor Armin Biere, Mitglied im Fahiem-Bacchus-Award-Auswahlkommittee und Informatikprofessor an der Albert-Ludwigs-Universität Freiburg.

"Ich fühle mich sehr geehrt, den ersten Fahiem-Bacchus Award erhalten zu haben. Es ermutigt mich wirklich, diese Forschung fortzusetzen und die Skalierbarkeit von Automated Reasoning in HPC- und Cloud-Systemen weiter voranzutreiben.", so Dominik Schreiber nach der Verleihung.

TalkaboutIT: Dominik Schreiber im Interview über seine Forschung am KIT, den Dissertationspreis und seine Zukunftspläne.