Back to Search
Start Over
Scalable SAT Solving in the Cloud
- Source :
- Theory and Applications of Satisfiability Testing – SAT 2021 ISBN: 9783030802226, SAT, Lecture Notes in Computer Science, Lecture Notes in Computer Science-Theory and Applications of Satisfiability Testing – SAT 2021
- Publication Year :
- 2021
- Publisher :
- Springer International Publishing, 2021.
-
Abstract
- Previous efforts on making Satisfiability (SAT) solving fit for high performance computing (HPC) have lead to super-linear speedups on particular formulae, but for most inputs cannot make efficient use of a large number of processors. Moreover, long latencies (minutes to days) of job scheduling make large-scale SAT solving on demand impractical for most applications. We address both issues with Mallob, a framework for job scheduling in the context of SAT solving which exploits malleability, i.e., the ability to add or remove processing power from a job during its computation. Mallob includes a massively parallel, distributed, and malleable SAT solving engine based on Hordesat with a more succinct and communication-efficient approach to clause sharing and numerous further improvements over its precursor. For example, Mallob on 640 cores outperforms an updated and improved configuration of Hordesat on 2560 cores. Moreover, Mallob can also solve many formulae in parallel while dynamically adapting the assigned resources, and jobs arriving in the system are usually initiated within a fraction of a second.<br />Comment: This preprint has not undergone peer review or any post-submission improvements or corrections. The Version of Record of this contribution is published in the proceedings of the International Conference on Theory and Applications of Satisfiability Testing 2021 (pp. 518-534), Springer, Cham, and is available online at https://doi.org/10.1007/978-3-030-80223-3_35
- Subjects :
- FOS: Computer and information sciences
Job scheduler
Computer Science - Logic in Computer Science
Computer science
business.industry
DATA processing & computer science
Malleable load balancing
Context (language use)
Cloud computing
Parallel computing
computer.software_genre
Supercomputer
Distributed computing
Satisfiability
Logic in Computer Science (cs.LO)
Computer Science - Distributed, Parallel, and Cluster Computing
Malleability
Scalability
Distributed, Parallel, and Cluster Computing (cs.DC)
ddc:004
business
Massively parallel
computer
Parallel SAT solving
Subjects
Details
- ISBN :
- 978-3-030-80222-6
978-3-030-80223-3 - ISSN :
- 03029743 and 16113349
- ISBNs :
- 9783030802226 and 9783030802233
- Database :
- OpenAIRE
- Journal :
- Theory and Applications of Satisfiability Testing – SAT 2021 ISBN: 9783030802226, SAT, Lecture Notes in Computer Science, Lecture Notes in Computer Science-Theory and Applications of Satisfiability Testing – SAT 2021
- Accession number :
- edsair.doi.dedup.....27c9d0073540ce303fb60b8f99f569b3