Recent Releases of Mallob
Mallob - v2.0.0
With version 2.0.0, we are releasing Mallob under a dual license, giving users the choice between the prior LGPL license and the MIT license.
Since its last release, Mallob has undergone significant enhancements and introduced many new features, including (but not limited to) the following:
SAT solving
- Improvements to clause sharing, including careful controlling of sharing volume and unlimited sharing of units (see our JAIR'24 article and SAT Comp. 2024 solver description)
- Updated sequential SAT solver backends (particularly CaDiCaL and Kissat)
- Improved, low-latency support for distributed incremental SAT solving (via Lingeling and CaDiCaL)
- Introduction of a "plain" flavor to SAT solver backends
- "SATWITHPRE" application mode for coordinated a-priori preprocessing (see our SAT'25 paper)
Proof technology
- Distributed production of monolithic proofs of unsatisfiability (see our TACAS'23 paper and JAR'25 article)
- Stand-alone efficient LRUP checker executable, capable of operating on 64-bit LRUP IDs and checking inverted proofs (allowing Mallob to skip un-inverting the proof)
- Distributed real-time proof checking with ImpCheck (see our SAT'24 paper and the ImpCheck repository)
Application engines
- Modular architecture for easily adding new application engines to Mallob
- Generic
SatJobStreaminterface for applications to spawn (incremental) SAT tasks, including a latency-hiding sequential solver thread - Prototypical distributed MaxSAT engine: Solution improving search via parallel interval search over admissible cost bounds (see our SoCS'25 paper)
- Experimental SMT solving engine via Bitwuzla (in an early stage, to be published)
- Various new options for job-internal communication
Job scheduling and communication
- Introduction of client-side application engines, which run on a single process and can spawn other (sub-)tasks of their own
- Ability to submit jobs by sending job submissions to another client process
- New interface for sending MPI messages from non-main threads
- Overhaul and simplification of serialized job description payloads, particularly for SAT
- RAII based communication via
MessageSubscriptionobjects with callbacks and other goodies - Adjustments and enhancements of job request matching algorithms in the background
- Introduction of a mechanism for caching, reusing, and sharing job descriptions in shared memory
Development
- Improved handling of memory panics and better resource management
- Extensive refactoring of core logic for better modularization and performance
Documentation
- External documentation for development, debugging, and application engines, also including guides for running Mallob on clusters and some FAQs
- Educational dummy implementations for certain kinds of application engines
- Adjustments to logging for better clarity and reduced verbosity
Scientific Software - Peer-reviewed
- C++
Published by domschrei 7 months ago
