scuttle
| Crates.io | scuttle |
| lib.rs | scuttle |
| version | 0.3.1 |
| source | src |
| created_at | 2023-07-12 08:32:29.308265 |
| updated_at | 2024-08-07 10:03:45.43774 |
| description | A multi-objective MaxSAT solver. |
| homepage | |
| repository | https://github.com/chrjabs/scuttle |
| max_upload_size | |
| id | 914371 |
| size | 5,213,006 |
Christoph Jabs (chrjabs)
documentation
README
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
- [1] Takehide Soh and Mutsunori Banbara and Naoyuki Tamura and Daniel Le Berre: Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation, CP 2017.
- [2] Miyuki Koshimura and Hidetomo Nabeshima and Hiroshi Fujita and Ryuzo Hasegawa: Minimal Model Generation with Respect to an Atom Set, FTP 2009.
- [3] Joao Cortes and Ines Lynce and Vasco M. Maquinho: New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization, TACAS 2023.
- [4] Christoph Jabs and Jeremias Berg and Andreas Niskanen and Matti Järvisalo: MaxSAT-Based Bi-Objective Boolean Optimization, SAT 2022.
- [5] Christoph Jabs and Jeremias Berg and Hannes Ihalainen and Matti Järvisalo: Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization, CP 2023.
- [6] Christoph Jabs and Jeremias Berg and Matti Järvisalo: Core Boosting in SAT-Based Multi-Objective Optimization, CPAIOR 2024.