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 with its SAT solving engine MallobSat is leading the respective (massively) parallel tracks of the International SAT Competition since 2020.

Each SAT solving task in Mallob can be incremental (allowing for efficient interactive solving procedures over evolving formulas) and can produce and/or check proof information (offering full confidence in each obtained result).

Mallob's flexible and decentralized approach to job scheduling allows to concurrently process many tasks of varying priority by different users.

Building upon Mallob's job scheduling and SAT solving capabilities, Mallob also features engines for state-of-the-art distributed MaxSAT solving (MallobMax) and bit-precise SMT solving (Bitwuzllob - parallelizing Bitwuzla).

This README provides some basic information and quick instructions for popular use cases of Mallob. Please also consult Mallob's full documentation, with docs/README.md as an entry point.

Mallob uses MPI (Message Passing Interface) and is built using CMake.

For a default, full featured build, execute bash scripts/setup/cmake-make.sh build in this (Mallob base) directory. For a minimal build, prepend MALLOB_MINIMAL=1 (and then append optional additions to the build as desired).

Find detailed instructions, including dependencies, at docs/setup.md.

We also provide a setup based on Docker containerization. Please consult the (for now separate) documentation in the docker/ directory.

Quick Start:

If you just want to use Mallob on a single, parallel machine, then the script scripts/run/mallob_local.sh automatically retrieves a suitable process+thread configuration of Mallob for your hardware that makes use of the entire machine. Useful presets can be applied by calling the scripts at config/presets/. Examples:

# SAT solving (default, simple setup)
scripts/run/mallob_local.sh -mono=instances/r3unsat_300.cnf
# SAT solving (similar to SAT Competition 2026 winning configuration, with Satsuma)
scripts/run/mallob_local.sh $(config/presets/sat-cascading-quick) -mono=instances/r3unsat_300.cnf
# SAT solving (with Satsuma and compositional proof production)
scripts/run/mallob_local.sh $(config/presets/sat-cascading-safe) -mono=instances/r3unsat_300.cnf
# SAT solving (with real-time proof/model checking)
scripts/run/mallob_local.sh $(config/presets/sat-realtimecheck) -mono=instances/r3unsat_300.cnf
# SMT solving
scripts/run/mallob_local.sh $(config/presets/smtcomp26) -mono=path/to/problem.smt2
# MaxSAT solving
scripts/run/mallob_local.sh -mono=path/to/problem.wcnf -mono-app=MAXSAT

More general settings:

Run build/mallob --help for an overview of all Mallob options.

E.g., to run MallobSat with one single (MPI) process with twelve Kissat threads, you can execute build/mallob -mono=path/to/problem.cnf -t=12 -satsolver=k.

For multi-process and distributed execution, prepend the command by mpirun or mpiexec followed by appropriate MPI options, as returned by the script scripts/run/mallob_local.sh (see above). 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 --bind-to core --map-by ppr:8:node:pe=4 -np 8 build/mallob -t=4

Find more detailed instructions at docs/execute.md.
For trouble-shooting, see also FAQ:Execution.

Find detailed instructions at docs/develop.md.

See CONTRIBUTING.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, excluded from compilation by default - see below.)

Depending on the application engines included in the particular build, the Mallob executable includes a number of liberally licensed solvers and/or (pre-)processors, which are listed at the top of every Mallob execution output together with their main authors.
There is also a Glucose interface for Mallob, which is subject to the non-free license of (parallel-ready) Glucose. Notably, its usage in competitive events is restricted. This interface is however disabled by default.

Note that a full build of Mallob may also download and build GPL-licensed software, which is then called by Mallob as external software (i.e., not compiled or integrated into the Mallob codebase). As of August 2026, this specifically concerns the Satsuma dependency Cliquer.

Within our codebase we further 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 / recent among this list of publications (all Open Access). A good, recent candidate is CAV'26.

• Mallob IPASIR Bridge for incremental SAT solving
• ImpCheck - Immediate Massively Parallel Propositional Proof Checking
• Comprehensive 2023 Experimental data at Zenodo
• Mallob at Helmholtz Research Software Directory (RSD)