Scalable SAT Solving and its Application

Das 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, die Unerfüllbarkeit der Formel 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 dieser Arbeit widmen wir uns einer Reihe von Herausforderungen zur Skalierbarkeit von angewandtem SAT Solving, geleitet von drei zentralen Forschungsfragen: Wie können wir moderne verteilte Rechenumgebungen effizient für SAT Solving nutzen? Wie können wir Systeme für SAT Solving in derartigen Umgebungen vollständig vertrauenswürdig machen, um deren Einsatz für kritische Anwendungen zu ermöglichen? Und: Wie können komplexe Anwendungen effizienteren Gebrauch von SAT-Solvern machen, damit zuvor unlösbare Probleme bewältigt werden können? Wir präsentieren Beiträge, die diese Fragen mit der Methodik des Algorithm Engineering angehen und dabei theoretische Überlegungen mit praktischer Entwicklungsarbeit verbinden.
... mehr
Zunächst untersuchen wir die effiziente Verteilung von SAT-Problemen und von ähnlichen Aufgaben mit unbekannter Ausführungszeit auf große verteilte Umgebungen. Insbesondere bei On-Demand-Computing wie High Performance Computing (HPC) oder Cloud-Diensten sind niedrige Latenzen und Reaktionszeiten ebenso erwünscht wie Ressourceneffizienz und Fairness. Wir stellen einen dezentralen Scheduling-Ansatz vor, der Verformbarkeit (malleability) ausnutzt, d.h. die Fähigkeit einer Berechnung, während ihrer Ausführung mit einer fluktuierenden Anzahl von Rechenressourcen umzugehen. Wir präsentieren vollständig skalierbare Algorithmen für unser Scheduling-Modell und implementieren praktisch effiziente Varianten dieser Algorithmen. In Experimenten mit bis zu 6144 Rechenkernen führt unser Ansatz zu Scheduling-Latenzen im Bereich von Millisekunden und erreicht eine nahezu optimale Systemauslastung.
Zweitens untersuchen wir die effiziente Parallelisierung von SAT Solving selbst. Insbesondere entwerfen wir einen kompakten Ansatz für globalen Klauselaustausch, der für Tausende von Solvern geeignet ist. In Experimenten mit bis zu 3072 Kernen hat unser Ansatz in Kombination mit modernen sequentiellen Solvern die bisher höchsten berichteten Speedups von verteiltem anwendungsunabhängigem SAT Solving mehr als verdoppelt. Unser Ansatz hat die Cloud-Kategorie (1600 logische Kerne) der renommierten International SAT Competition vier Jahre in Folge dominiert und sich auch auf moderat paralleler Hardware (64 logische Kerne) als äußerst konkurrenzfähig erwiesen. Innerhalb unseres Scheduling-Systems zeigen wir, dass die Kombination aus paralleler Jobverarbeitung und verformbarem SAT Solving ansprechende Speedups bei gleichzeitig guter Ressourceneffizienz erzielen kann.
Drittens befassen wir uns mit einer großen Einschränkung der meisten parallelen und verteilten SAT-Solver, nämlich ihrer Unfähigkeit, Beweise für Unerfüllbarkeit zu erzeugen, was ihre Vertrauenswürdigkeit einschränkt. Wir stellen den ersten praktikablen und skalierbaren Ansatz zur Erzeugung solcher Zertifikate bei massiv parallelem SAT Solving vor. Gewissermaßen spult unser verteilter Algorithmus den Lösungsvorgang in der Zeit zurück und verfolgt den Ursprung aller relevanten geteilten Klauseln. Mit einem vertretbaren Zusatzaufwand im Vergleich zu unserem Solver ohne Beweis-Erzeugung ist dieser Ansatz in der Lage, effizient Beweise auszugeben, die viele Gigabytes an komprimierter Information enthalten.
Zu guter Letzt berichten wir von einer umfangreichen Fallstudie zu angewandtem SAT Solving. Konkret stellen wir einen SAT-basierten Ansatz für die Planung von hierarchischen Aufgabennetzwerken mit totaler Ordnung (Totally Ordered Hierarchical Task Networks, TOHTN) vor — ein beliebter Zweig der automatisierten Planung, der reichhaltige Möglichkeiten für die Modellierung komplexer hierarchischer Planungsaufgaben bereit hält. Wir präsentieren die erste SAT-Kodierung von TOHTN-Problemen, die eine geliftete, d.h. parametrisierte Problembeschreibung beibehält und daher die kombinatorische Vergrößerung der Eingabe vermeidet, die andere SAT-basierte Ansätze mit sich bringen. Mit einem integrierten Ansatz, der zwischen Kodierung und inkrementellem SAT Solving alterniert, erzeugt unser Ansatz Formeln, die im Vergleich zu vorherigen SAT-basierten Ansätzen oft um ein bis zwei Größenordnungen kleiner sind. Wir stellen auch eine Möglichkeit vor, hierarchische Planungsprobleme auf paralleler Hardware zu verarbeiten, indem wir unser Scheduling- und SAT-Solving-System verwenden. Im Rahmen dieser Bemühung haben wir unser System um die Unterstützung von inkrementellem SAT Solving erweitert, was es zum ersten inkrementellen SAT-Solver für große Systeme macht.
Insgesamt hat unsere Arbeit zu erheblichen Fortschritten bei skalierbarem SAT Solving und dessen effizienter Anwendung geführt. Damit erweitern wir den Horizont der logischen Probleme, die in modernen Rechenumgebungen praktikabel lösbar sind.

The problem of propositional satisfiability (SAT) is to find a variable assignment for a given propositional formula such that the formula evaluates to true or, if no such assignment exists, to report that the formula is unsatisfiable. SAT solving has attracted a great deal of attention due to its theoretical significance, its generic nature, and its broad applicability to a wide range of problems. In this work, we target a number of scalability challenges in the realm of applied SAT solving, guided by three research questions: How can we efficiently exploit modern distributed computing environments for SAT solving? How can we render SAT solving systems in such environments trustworthy for critical applications? And: How can complex applications make more efficient use of SAT solvers in order to handle previously infeasible inputs? We present contributions which address these questions with the methodology of algorithm engineering, combining theoretic considerations with practical engineering.
... mehr
First, we investigate the efficient scheduling of SAT tasks and other tasks with unknown execution time in large distributed environments. Especially in on-demand computing such as high performance computing (HPC) or cloud services, low scheduling latencies and response times are desirable as well as resource efficiency and fairness. We derive a decentralized scheduling approach which exploits malleability, i.e., the ability of a task to handle a fluctuating amount of computational resources during its execution. We derive fully scalable algorithms for our scheduling model and implement practically efficient variations of them. In experiments on up to 6144 cores, our approach results in scheduling latencies in the range of milliseconds and achieves near-optimal system utilization.
Secondly, we explore the efficient parallelization of SAT solving itself. In particular, we design a compact all-to-all clause sharing scheme which scales to thousands of solvers. In experiments on up to 3072 cores, our approach combined with state-of-the-art solver backends more than doubles the previously highest reported speedups in general-purpose distributed SAT solving. Our approach has dominated the cloud track (1600 hardware threads) of the renowned International SAT Competition four years in a row while also proving highly competitive on a moderately parallel scale (64 hardware threads). Within our job scheduling framework, we show that the combination of parallel job processing and malleable SAT solving can achieve appealing speedups while retaining good resource efficiency.
Thirdly, we address a major shortcoming of most parallel and distributed solvers, namely their inability to produce certificates of unsatisfiability which limits their trustworthiness. We propose the first feasible and scalable approach to generating proof certificates in massively parallel SAT solving. Our distributed algorithm essentially rewinds the solving procedure and tracks the origin of all relevant shared clauses. With reasonable overhead compared to our non proof producing solver, this approach is able to efficiently generate proofs holding many gigabytes of compressed information.
Last but not least, we conduct a major case study on applied SAT solving. Specifically, we present a SAT-based approach to Totally Ordered Hierarchical Task Network (TOHTN) planning—a popular branch of automated planning which provides a rich framework to model complex hierarchical tasks. We present the first SAT encoding of TOHTN problems which preserves a lifted, i.e., parametrized, problem description and therefore avoids the combinatorial blowup which other SAT-based approaches introduce. With an integrated approach that alternates between encoding and incremental SAT solving, our approach generates formulas which are oftentimes smaller by one to two orders of magnitude compared to prior SAT-based approaches. We also present a way to process hierarchical planning problems on parallel hardware using our job scheduling and malleable SAT solving framework. For this means, we enable our system to support incremental SAT solving, rendering it the first large-scale incremental SAT solver.
Put together, our work has led to substantial advances in scalable SAT solving and its efficient application. We thus push the frontier of automated reasoning problems that are feasible to solve in modern computing environments.