#solver #sat-solver #multi-objective #maxsat

bin+lib scuttle

A multi-objective MaxSAT solver

4 releases (2 breaking)

0.3.1 Aug 7, 2024
0.3.0 Feb 23, 2024
0.2.0 Sep 5, 2023
0.1.0 Jul 12, 2023

#543 in Math

MIT license

1MB
6.5K SLoC

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 our CP'23 paper on preprocessing for multi-objective optimization [5] and our CPAIOR'24 paper on core boosting [6]. Additional material for the CP'23 paper can be found here while material for the CPAIOR'24 paper is available in the cpaior24/ directory in this repository.

Algorithms

First argument Description
p-minimal P-Minimal model enumeration as described in [1] and [2]
lower-bounding Lower-bounding search as described in [3] (called "core-guiding" there)
bioptsat Sat-Unsat variant of the BiOptSat algorithm described in [4]

Building

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

To build the project from source, you will need to clone RustSAT and MaxPre-rs within the same workspace directory as this repository.

workspace/
├── maxpre-rs/
├── rustsat/
└── scuttle/

You can then build scuttle by running cargo build within workspace/scuttle/.

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.

Dependencies

~6–18MB
~200K SLoC