Scalable SAT Solving in the Cloud

TL;DR

This paper introduces Mallob, a scalable, malleable SAT solving framework for cloud environments that efficiently manages resources and outperforms previous systems like Hordesat on large core counts.

Contribution

Mallob presents a novel, communication-efficient, malleable SAT solver framework that dynamically adapts to resources and significantly improves scalability and performance.

Findings

Mallob outperforms Hordesat on 640 cores versus 2560 cores.

It can solve many formulae in parallel with dynamic resource adaptation.

Jobs are initiated within a fraction of a second.

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.