Scuttle - A Multi-Objective MaxSAT Solver in Rust

Scuttle is a multi-objective MaxSAT solver written in Rust and based on the RustSAT library and the CaDiCaL SAT solver.

Publications

This solver was used in the following publications. For each publication, a tag (specified in brackets) marks the exact revision used:

• CP'23 (cp23): "Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization" [5]. Additional material here.
• CPAIOR'24 (cpaior24): "Core Boosting in SAT-Based Multi-Objective Optimization" [6]. Additional material in cpaior24/.
• TACAS'25 (tacas25): "Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability" [7]. Additional material in tacas25/.

Algorithms

Building

Note: Scuttle requires nightly Rust, which can be installed via rustup.

If you simply want a binary of the solver, you can install it from crates.io by running cargo +nightly install --locked scuttle.

To build the project from source, make sure to initialize the git submodules with git submodule update --init --recursive. You can then build scuttle by running cargo +nightly build.

By default, MaxPre preprocessing is not included in the build anymore. To include preprocessing with MaxPre, add --features=maxpre.

Features

• sol-tightening: includes heuristic tightening of solutions after they are found in the build
• maxpre: includes preprocessing with MaxPre in the build

What's The Name

Apparently "scuttle" is one of multiple term for a group of crabs, which seemed fitting for a multi-objective solver in Rust.

References

• Takehide Soh and Mutsunori Banbara and Naoyuki Tamura and Daniel Le Berre: Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation, CP 2017.
• Miyuki Koshimura and Hidetomo Nabeshima and Hiroshi Fujita and Ryuzo Hasegawa: Minimal Model Generation with Respect to an Atom Set, FTP 2009.
• Joao Cortes and Ines Lynce and Vasco M. Maquinho: New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization, TACAS 2023.
• Christoph Jabs and Jeremias Berg and Andreas Niskanen and Matti Järvisalo: MaxSAT-Based Bi-Objective Boolean Optimization, SAT 2022.
• Christoph Jabs and Jeremias Berg and Hannes Ihalainen and Matti Järvisalo: Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization, CP 2023.
• Christoph Jabs and Jeremias Berg and Matti Järvisalo: Core Boosting in SAT-Based Multi-Objective Optimization, CPAIOR 2024.
• Christoph Jabs and Jeremias Berg and Bart Boergarts and Matti Järvisalo: Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability, TACAS 2025.