-ffffbb){kind=icon}
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.
The source code of Mallob can be used, changed and redistributed under the terms of the Lesser General Public License (LGPLv3), one exception being the Glucose interface which is excluded from compilation by default (see below). Please approach us if you require a deviating license.
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 the proof-related tools which are included and/or fetched in the tools/ directory.
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:
- robin-map by Thibaut Goetghebuer-Planchon, for efficient unordered maps and sets
- libcuckoo by Manu Goyal et al., for concurrent hash tables
- JSON for Modern C++ by Niels Lohmann, for reading and writing JSON files
- Compile Time Regular Expressions by Hana Dusíková, for matching particular user inputs
- robin_hood hashing by Martin Ankerl, for efficient unordered maps and sets
If you make use of Mallob in an academic setting or in a competitive event, please cite the most relevant among the following publications.
@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}
}@InProceedings{michaelson2023unsatisfiability,
author={Michaelson, Dawn and Schreiber, Dominik and Heule, Marijn J. H. and Kiesl-Reiter, Benjamin and Whalen, Michael W.},
title={Unsatisfiability proofs for distributed clause-sharing SAT solvers},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
year={2023},
organization={Springer},
pages={348--366},
doi={10.1007/978-3-031-30823-9_18},
}@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{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},
note={\url{http://hdl.handle.net/10138/584822}},
}@phdthesis{schreiber2023scalable,
author={Dominik Schreiber},
title={Scalable {SAT} Solving and its Application},
year={2023},
school={Karlsruhe Institute of Technology},
doi={10.5445/IR/1000165224}
}