SAtRes    Research    The Mallob System

The Mallob System

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.


Logo of the Mallob system


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.

References

The following list names some of the most important publications on Mallob. All publications on Mallob can be found at our publications page.

  1. The original publication on Mallob, with a strong focus on SAT solving:
    Scalable SAT Solving in the Cloud. Schreiber, D., & Sanders, P. In Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), pages 518–534, 2021. Springer
  2. A detailed presentation of our decentralized and flexible scheduling algorithms, using SAT solving as a case study:
    Decentralized online scheduling of malleable NP-hard jobs. Sanders, P., & Schreiber, D. In Int. European Conf. on Parallel Processing (Euro-Par), pages 119–135, 2022. Springer
  3. In-depth journal article on Mallob’s SAT solving engine MallobSat:
    MallobSat: Scalable SAT Solving by Clause Sharing. Schreiber, D., & Sanders, P. Journal of Artificial Intelligence Research (JAIR) 80, pages 1437-1495, 2024.
  4. Full documentation and reference of Mallob’s features and capabilities (up to fall 2023), including proofs of unsatisfiability and incremental solving:
    Scalable SAT Solving and its Application. Schreiber, D. Doctoral Thesis, Karlsruhe Institute of Technology (KIT), 2023.