SAT'26 - Scuttle

Abstract

We describe the Scuttle system for multi-objective combinatorial optimization. Scuttle accepts multi-objective instances where the constraints are declared either as propositional clauses or pseudo-Boolean constraints, and implements a range of multi-objective maximum satisfiability algorithms (including ones for enumerating all Pareto-optimal and leximax-optimal solutions). Pseudo-Boolean constraints are translated to clauses, allowing for applying any of the implemented algorithms on both the clausal and the pseudo-Boolean level.Scuttle also includes tightly integrated preprocessing (both core boosting and liftings of SAT preprocessing techniques) for multi-objective instances and can provide proof certificates for selected algorithms.

Bibtex

@inproceedings{JabsEtAl2026ScuttleMultiObjective,
  author = {Jabs, Christoph and Berg, Jeremias and Järvisalo, Matti},
  title = {Scuttle: {A} System for Multi-Objective MaxSAT},
  booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2026},
  year = {2026},
  month = jul,
  editor = {Ignatiev, Alexey and Szeider, Stefan},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"u}r Informatik},
  volume = {377},
}