Schreiber, DominikReischuk, Rüdiger2024-10-022024-10-022024978-3-88579-982-5https://dl.gi.de/handle/20.500.12116/44725Das Problem der aussagenlogischen Erfüllbarkeit (Propositional Satisfiability, SAT) besteht darin, eine Variablenbelegung für eine gegebene aussagenlogische Formel zu finden, sodass die Formel “wahr” ergibt, oder, wenn keine solche Belegung existiert, Unerfüllbarkeit zu attestieren. Das Lösen derartiger Probleme, genannt SAT Solving, hat aufgrund seiner theoretischen Bedeutung, seiner generischen Natur und seiner breiten Anwendbarkeit auf eine Vielzahl von Problemen viel Beachtung erlangt. In der vorgestellten Dissertation widmen wir uns einer Reihe von Herausforderungen zur Skalierbarkeit von SAT Solving in modernen Rechenumgebungen. Zunächst stellen wir einen dezentralen und flexiblen Ressourcenzuteilungs-Ansatz vor, um viele SAT-Aufgaben zu gleich möglichst effizient zu lösen. Zweitens präsentieren wir ein vielfach ausgezeichnetes System für paralleles und verteiltes SAT Solving und, damit verbunden, den ersten praktikablen Ansatz, aus derartigen Systemen Beweise der Unerfüllbarkeit zu gewinnen. Zuletzt stellen wir in einer Anwendungsstudie einen radikal neuartigen Ansatz für SAT-basiertes hierarchisches Planen vor.de10.18420/Diss2023-28