The platform Mallob (Malleable Load Balancer, or Massively Parallel Logic Backend) is a distributed platform for processing automated reasoning tasks in modern large-scale HPC and cloud environments. Mallob primarily solves instances of the NP-complete propositional satisfiability (SAT) problem – an essential building block at the core of automated reasoning and Symbolic AI. Mallob's flexible and decentralized approach to job scheduling allows to concurrently process many tasks of varying priority by different users. As such, Mallob can drastically improve your academic or industrial workflows tied to automated reasoning.

Mallob's tightly integrated distributed general-purpose SAT solving engine, which we refer to as MallobSat, has received a large amount of attention, five gold medals of the International SAT Competition's Cloud Track in a row, and Amazon's proposition that our system is, "by a wide margin, the most powerful SAT solver on the planet" (Byron Cook, Amazon Science blog post).
Mallob is also the first distributed system that supports incremental SAT solving, i.e., interactive solving procedures over evolving formulas. Most recently, Mallob spearheaded the adoption of unsatisfiability proof checking in parallel and distributed SAT solving. Since proofs can serve as crucial witnesses for a result’s correctness, Mallob is suitable even for the most critical use cases.

The Mallob system is liberally (LGPL) licensed and openly developed on Github, where detailed instructions for building, testing, and running Mallob can be found.

Background

Despite SAT being a notoriously difficult problem, practically efficient SAT solving approaches have empowered a wide range of real-world applications for SAT such as software verification, electronic design automation, cryptography, automated planning, explainable AI, and theorem proving. With respect to modern computing paradigms such as cloud computing and high-performance computing (HPC), the limited scalability of established parallel and distributed SAT solvers has become a pressing issue. Moreover, since processing times of SAT jobs are unknown in advance, conventional HPC scheduling approaches applied to such jobs can lead to prohibitively large scheduling latencies and to suboptimal utilization of computational resources. Instead, we make use of so-called malleable scheduling. A parallel computing task is called malleable if the amount of computational resources allotted (i.e., the number of cores or machines) can be adjusted during its execution. Malleability is a powerful paradigm in the field of job scheduling and load balancing as it allows to schedule incoming jobs rapidly and to continuously rebalance the present tasks according to their priority and other properties.

We believe that a distributed service which combines scalable SAT solving with malleable job scheduling can significantly improve many SAT-related academic and industrial workflows in terms of productivity and (resource-)efficiency. Moreover, our decentralized scheduling approach is applicable to further applications beyond SAT where processing times are unknown in advance and a modest amount of data is transferred in between the workers.

System Overview

Mallob is a C++ application designed for parallel and distributed systems between 16 and 10000 cores and allows to resolve propositional problems in a (massively) parallel manner. Our award-winning SAT solving engine scales up to three thousand cores using a selection of well-established sequential SAT solvers and a careful exchange of information among them.

Each distributed SAT solving task is malleable, allowing users to submit formulae to Mallob at will with scheduling latencies in the range of milliseconds. Computational resources are allotted proportional to each job's priority and also respecting each job's (maximum) demand of resources. Our scheduling approach is fully decentralized and uses a small part of each worker's CPU time (< 5%) to perform scheduling negotiations. As such, Mallob achieves optimal system utilization almost always, i.e., either all available processes are utilized or all resource demands are fully met. We achieve this feat by arranging each active job as a binary tree of workers and growing or shrinking each job tree dynamically based on the current system state. We describe these techniques in depth in our related publications.