Ph.D. Thesis, Karlsruher Institut für Technologie (KIT), Germany, 2023.
![Scalable SAT Solving and its Application [link]](https://bibbase.org/img/filetypes/link.svg "link")
Pdf doi abstract bibtex 40 downloads
Pdf doi abstract bibtex 40 downloads 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.
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.
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.
@PhdThesis{Schreiber2023Dissertation,
author = {Dominik Schreiber},
title = {Scalable SAT Solving and its Application},
school = {Karlsruher Institut für Technologie (KIT), Germany},
year = {2023},
abstract = {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.
<br><br>
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.
<br><br>
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.
<br><br>
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.
<br><br>
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.
<br><br>
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.},
doi = {10.5445/IR/1000165224},
url_PDF = {https://publikationen.bibliothek.kit.edu/1000165224/151802078}
}Downloads: 40