KIT | KIT-Bibliothek | Impressum | Datenschutz

Scalable SAT Solving in the Cloud

Schreiber, Dominik ORCID iD icon 1; Sanders, Peter ORCID iD icon 1
1 Institut für Theoretische Informatik (ITI), Karlsruher Institut für Technologie (KIT)


Previous efforts on making Satisfiability (SAT) solving fit for high performance computing (HPC) have led 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 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.

Postprint §
DOI: 10.5445/IR/1000132740
Veröffentlicht am 03.07.2022
DOI: 10.1007/978-3-030-80223-3_35
Zitationen: 6
Zitationen: 9
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2021
Sprache Englisch
Identifikator ISBN: 978-3-030-80223-3
ISSN: 0302-9743, 1611-3349
KITopen-ID: 1000132740
Erschienen in Theory and Applications of Satisfiability Testing – SAT 2021. Ed.: C.-M. Li
Veranstaltung 24th International Conference on Theory and Applications of Satisfiability Testing (2021), Barcelona, Spanien, 05.07.2021 – 09.07.2021
Verlag Springer
Seiten 518-534
Serie Lecture Notes in Computer Science (LNCS) ; 12831
Vorab online veröffentlicht am 02.07.2021
Schlagwörter Parallel SAT solving; Distributed computing; Malleable load balancing
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page