Mallob (Malleable Load Balancer, or Massively Parallel Logic Backend) is a distributed platform for automated reasoning in modern large-scale HPC and cloud environments. Mallob primarily solves instances of propositional satisfiability (SAT) – an essential building block at the core of 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 be used to scale up academic or industrial workflows tied to automated reasoning.
Mallob and its tightly integrated distributed general-purpose SAT solving engine, MallobSat, received a large amount of attention, including five gold medals in the International SAT Competition's Cloud Track in a row, high-profile scientific awards, and a highlight on Amazon Science. Mallob is the first distributed system that supports incremental SAT solving, i.e., interactive solving procedures over evolving formulas, and is also the first system transferring proof technology to parallel and distributed SAT solving in a scalable manner.
Mallob uses MPI (Message Passing Interface) and is built using CMake.
For a default quick-start build, execute scripts/setup/build.sh (and/or modify it as needed).
Find detailed instructions at docs/setup.md.
We also provide a setup based on Docker containerization. Please consult the (for now separate) documentation in the docker/ directory.
To enable bash auto-completion by pressing TAB, execute source scripts/run/autocomplete.sh from Mallob's base directory.
You should now be able to autocomplete program options by pressing TAB once or twice from this directory.
Quick Start:
Run build/mallob --help for an overview of all Mallob options.
E.g., to run MallobSat with a single (MPI) process with twelve Kissat threads, execute build/mallob -mono=path/to/problem.cnf -t=12 -satsolver=k. Make sure to execute Mallob from it's home directory, otherwise some relative paths might not work per default.
For trouble-shooting, see also FAQ:Execution.
For multi-process and distributed execution, prepend the command by mpirun or mpiexec followed by appropriate MPI options.
E.g., using Open MPI, the following command runs Mallob as a service (taking JSON job submissions on demand at .api/jobs.0/) with a total of eight processes à four threads.
RDMAV_FORK_SAFE=1; mpirun -np 8 --bind-to core --map-by ppr:1:node:pe=4 build/mallob -t=4Find detailed instructions at docs/execute.md.
Find detailed instructions at docs/develop.md.
First of all, please let us know if you make use of Mallob! We like to hear about it and depend on it for continued support and further development.
Mallob and its source code can be used, changed and redistributed under the terms of the MIT License or the Lesser General Public License (LGPLv3). One exception is the Glucose interface which is excluded from compilation by default (see below).
The used versions of Lingeling, YalSAT, CaDiCaL, and Kissat are MIT-licensed, as is HordeSat (the massively parallel solver system our SAT engine was based on) and other statically linked libraries (RustSAT, Bitwuzla, and MaxPRE).
The Glucose interface of Mallob (only included when explicitly compiled with -DMALLOB_USE_GLUCOSE=1) is subject to the non-free license of (parallel-ready) Glucose. Notably, its usage in competitive events is restricted.
Within our codebase we make thankful use of the following liberally licensed projects:
- Compile Time Regular Expressions by Hana Dusíková, for matching particular user inputs
- JSON for Modern C++ by Niels Lohmann, for reading and writing JSON files
- ringbuf by Mindaugas Rasiukevicius, for efficient ring buffers
- robin_hood hashing by Martin Ankerl, for efficient unordered maps and sets
- robin-map by Thibaut Goetghebuer-Planchon, for efficient unordered maps and sets
- SipHash C reference implementation by Jean-Philippe Aumasson, for Message Authentication during trusted distributed clause-sharing solving
If you make use of Mallob in an academic / scientific setting or in a competitive event, please cite the most relevant among the following publications (all Open Access).
@article{schreiber2024mallobsat,
title={{MallobSat}: Scalable {SAT} Solving by Clause Sharing},
author={Schreiber, Dominik and Sanders, Peter},
journal={Journal of Artificial Intelligence Research (JAIR)},
year={2024},
volume={80},
pages={1437--1495},
doi={10.1613/jair.1.15827},
}@inproceedings{sanders2022decentralized,
title={Decentralized Online Scheduling of Malleable {NP}-hard Jobs},
author={Sanders, Peter and Schreiber, Dominik},
booktitle={International European Conference on Parallel and Distributed Computing},
pages={119--135},
year={2022},
organization={Springer},
doi={10.1007/978-3-031-12597-3_8}
}@article{michaelson2025producing,
author={Michaelson, Dawn and Schreiber, Dominik and Heule, Marijn J. H. and Kiesl-Reiter, Benjamin and Whalen, Michael W.},
title={Producing Proofs of Unsatisfiability with Distributed Clause-Sharing {SAT} Solvers},
journal={Journal of Automated Reasoning (JAR)},
year={2025},
organization={Springer},
volume={69},
doi={10.1007/s10817-025-09725-w},
}@inproceedings{schreiber2024trusted,
title={Trusted Scalable {SAT} Solving with on-the-fly {LRAT} Checking},
author={Schreiber, Dominik},
booktitle={Theory and Applications of Satisfiability Testing (SAT)},
year={2024},
pages={25:1--25:19},
organization={Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
doi={10.4230/LIPIcs.SAT.2024.25},
}@inproceedings{schreiber2025from,
author={Schreiber, Dominik and Jabs, Christoph and Berg, Jeremias},
title={From Scalable {SAT} to {MaxSAT}: Massively parallel Solution Improving Search},
booktitle={Symposium on Combinatorial Search (SoCS)},
year={2025},
doi={10.1609/socs.v18i1.35984},
volume={18},
number={1},
pages={127--135},
}@inproceedings{schreiber2024mallob,
title={{MallobSat} and {MallobSat-ImpCheck} in the {SAT} Competition 2024},
author={Schreiber, Dominik},
booktitle={SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions},
year={2024},
pages={21--22},
url={http://hdl.handle.net/10138/584822},
}@misc{schreiber2025distributed,
title={Distributed Incremental {SAT} Solving with {Mallob}: Report and Case Study with Hierarchical Planning},
author={Dominik Schreiber},
year={2025},
eprint={2505.18836},
archivePrefix={arXiv},
primaryClass={cs.DC},
url={https://arxiv.org/abs/2505.18836},
}