Karlsruher Hochleistungs-Lösungsverfahren für Logik besteht im internationalen Wettbewerb.
Das Hochleistungs-Lösungsverfahren "mallob" für logische Probleme von Dominik Schreiber aus der Arbeitsgruppe Algorithmik II (Prof. Peter Sanders) hat im Cloud Track der internationalen SAT Competition 2020 mit deutlichem Vorsprung den ersten Platz erzielt.
Bei diesem internationalen Wettbewerb für aussagenlogische Erfüllbarkeit, englisch SAT Solving (von Satisfiability), geht es um die weltweit effizientesten Lösungsverfahren für Probleme, die in formaler Logik dargestellt werden können. Die SAT Competition ist regelmäßiger Bestandteil der jährlich stattfindenden "International Conference on Theory and Applications of Satisfiability Testing". Die Konferenz ist Treffpunkt international führender Forscherinnen und Forscher im Bereich logischer Berechnungen. Ziel des Wettbewerbs ist es, Entwicklerinnen und Entwicklern solcher SAT Solver einen Anreiz zu geben, ihre Beiträge einem breiten Publikum zu präsentieren und damit den Stand der Technik sowie deren Einsatz in Industrie und Forschung voranzutreiben. Die Prüfung auf aussagenlogische Erfüllbarkeit ist ein bekanntermaßen schwieriges Problem aus der theoretischen Informatik, das aufgrund seiner generischen Problemstruktur in einer Fülle von Anwendungen Verwendung findet, darunter Software- und Hardwareverifikation, automatisierte Planung, Kryptographie, automatische Beweisführung und Schaltkreisdesign.
Der Cloud Track des Wettbewerbs ist dessen jüngste und modernste Wertungskategorie, welche die teilnehmenden Programme anhand ihrer Fähigkeit bewertet, in einer Hochleistungsrechenumgebung schnell und effizient logische Probleme aufzulösen. Jedes Programm wurde auf 100 leistungsstarken Rechenknoten der Amazon Web Services (AWS) Cloud zugleich ausgeführt, die es auf insgesamt 800 physische bzw. 1600 logische Rechenkerne bringen. Bei einem Zeitlimit von 1000 Sekunden pro Instanz stehen somit über 440 CPU-Stunden für jedes der logischen Probleme zur Verfügung, was den fünffachen Rechenressourcen gegenüber der nächstkleineren Wertungskategorie entspricht, dem Lösungsverfahren jedoch auch weniger Echtzeit pro Instanz lässt.
Dominik Schreibers Ansatz „mallob“ löste 306 der 400 Logik-Probleme vielfältigen Ursprungs erfolgreich, womit „mallob“ über alle Wertungskategorien des Wettbewerbs hinweg die meisten Instanzen lösen konnte. Die nächstplatzierten Mitbewerber des Cloud Tracks namens TopoSAT2 und Slime lösten 283 bzw. 239 Instanzen und benötigten für gelöste Instanzen im Schnitt merklich mehr Zeit als „mallob“, was sich jeweils in der ausschlaggebenden Punktewertung niederschlug.
Das Framework „mallob“ ist für das Lösen vieler aussagenlogischer Instanzen zugleich konzipiert, konnte hier jedoch mit seiner speziellen Konfiguration "mallob-mono" im schnellen Lösen einzelner Instanzen überzeugen. Auf technischer Seite basiert das Lösungsverfahren auf dem Hochleistungs-Solver HordeSat von Peter Sanders, Tomáš Balyo und Carsten Sinz (2015), der im Hintergrund viele Solver gleichzeitig arbeiten lässt und dabei gezielt Informationen zwischen den Solvern austauscht. „Mallob“ bringt jedoch erhebliche Änderungen mit sich, die unter anderem den Aufwand für Kommunikation zwischen den Rechenknoten deutlich reduzieren und damit den Solvern im Hintergrund mehr Gelegenheit für das eigentliche logische Schließen geben. Eine weitere erfolgreiche Änderung ist die Integration randomisierter Lösungsverfahren, sogenannter Local Search Solver, die deutlich anders als konventionelle SAT Solver funktionieren und damit das Portfolio verwendeter Lösungsstrategien effektiv erweitern. Das Framework wird für alle Interessierten als Open-Source-Software zur freien Verfügung gestellt werden.
Dominik Schreiber beschäftigt sich seit seiner 2018 in Grenoble verfassten Masterarbeit mit SAT Solving und arbeitet momentan im Rahmen seiner Dissertation an skalierbaren Verfahren und effizienter Lastverteilung für automatisiertes logisches Schließen und für dessen Anwendungen.
Präsentation der Resultate (Slides):
https://satcompetition.github.io/2020/downloads/satcomp20slides.pdf#page=36
Website der SAT Competition 2020:
https://satcompetition.github.io/2020/
Website der SAT Conference 2020:
https://sat2020.idea-researchlab.org