Multi-objective Maximum Satisfiability by Single-objective Implicit Hitting Set Optimization

Abstract

Significant advances in practical approaches to maximum satisfiability (MaxSAT) solving have made MaxSAT a viable approach to solving complex NP-hard combinatorial optimization problems. Several recent works have extended single-objective MaxSAT algorithms to the multi-objective setting, enabling the enumeration of Pareto-optimal solutions for problems expressed as multi-objective MaxSAT (MO-MaxSAT). We propose and instantiate an alternative approach to MO-MaxSAT solving. Phrased as an implicit hitting set (IHS) approach, our algorithm works by iteratively invoking a single-objective IHS oracle on a scalarization of the multi-objective instance at hand. Our open-source implementation significantly outperforms an earlier-proposed IHS-style approach and complements the current state of the art in algorithmic approaches to MO-MaxSAT.

Bibtex

@inproceedings{pareto-ihs,
  author = {Jabs, Christoph and Berg, Jeremias and J{\"a}rvisalo, Matti},
  title = {Multi-objective Maximum Satisfiability by Single-objective Implicit Hitting Set Optimization},
  booktitle = {Integration of Constraint Programming, Artificial Intelligence, and Operations Research---23rd International Conference, {CPAIOR} 2026, Rabat, Morocco, May 26--29, 2026},
  year = {2026},
  editor = {Guns, Tias},
}