News
Mallob 2.0: MIT ReleaseMallob 2.0: MIT Release
July 31, 2025
We are excited to announce the 2.0 release of Mallob (Malleable Load Balancer / Massively Parallel Logic Backend).
With this major release, our flagship software for job scheduling and large-scale automated reasoning receives an MIT license, one of the most permissive open source software licenses and, in particular, without the weak copyleft restriction from earlier LGPL licensed releases. With this step, Mallob aligns its licensing with many other world-leading automated reasoning tools like CaDiCaL, Kissat, or Z3. LGPL remains an alternative licensing option (dual license). Regardless of this change, we are always eager to hear about people using and applying our solutions, so please do let us know if you make use of Mallob!
Since its last release, Mallob has undergone significant enhancements and introduced many new features, including (but not limited to) the following list.
SAT Solving
We’ve made significant improvements to MallobSat’s clause sharing, including reliable distributed filtering of obsolete clauses, automated controlling of the sharing volume, and the ability to share clauses below a certain length without limits. For more details, we refer to our JAIR'24 article and the SAT Competition 2024 solver description. The sequential SAT solver backends, particularly CaDiCaL and Kissat, have been updated to enhance performance.
A key feature in this update is comprehensive support for distributed incremental SAT solving, which now offers stable and low-latency solving performance (using Lingeling and CaDiCaL).
We’ve also introduced the “SATWITHPRE” application mode for coordinated preprocessing, as discussed in our SAT'25 paper. Additionally, a “plain” flavor has been added to the SAT solver backends to omit any pre-/inprocessing during parallel solving.
Proof Technology
This release includes cutting-edge distributed proof technology. MallobSat now supports the distributed production of (monolithic, post-mortem) proofs of unsatisfiability, as detailed in our TACAS'23 paper and JAR'25 article. A new stand-alone LRUP checker executable is included, capable of handling 64-bit LRUP IDs and checking inverted proofs, which allows Mallob to skip the proof un-inverting process.
We’ve also integrated distributed real-time proof checking – see our SAT'24 paper and the ImpCheck repository. This setup validates all reasoning steps via dedicated, independent checker processes that run next to solving. Checkers compute cryptographic fingerprints for validated clauses to transfer correctness guarantees across different checkers without relying on the distributed program’s correctness.
Due to the required proof format (LRUP), only CaDiCaL is supported as a solver backend for proof-producing setups as of now.
Application Engines
A prototypical distributed MaxSAT solving engine is included in this release. It uses parallel interval search over admissible cost bounds to improve solutions, as discussed in our SoCS'25 paper. This engine makes extensive use of Mallob’s multi-tasking, sub-tasking, and incremental SAT solving capabilities.
The architecture of Mallob has been updated to make it easier to add new application engines. This release introduces client-side application engines, which run on a single process and can spawn sub-tasks on their own. For this purpose, the new SatJobStream interface allows applications to create incremental SAT tasks efficiently, including a “latency-hiding” internal solver thread.
Jobs can now be submitted by sending job submissions to another (client) process. A new interface for sending MPI messages from non-main threads has been introduced to simplify communication-related logic. We’ve also introduced RAII-based MessageSubscription objects with convenient callbacks for when a message arrives. Various new options for job-internal communication have been added to increase convenience and flexibility.
Documentation
The release includes comprehensive external documentation for development, debugging, and application engines, along with guides for running Mallob on clusters and some FAQs. We’ve added educational dummy implementations for certain application engines to help users get started.
You can find Mallob, as always, at our research page or directly on GitHub.