CPAIOR'24 - Core Boosting for MO-MaxSAT

Abstract

Maximum satisfiability (MaxSAT) constitutes today a successful approach to solving various types of real-world optimization problems through propositional encodings. Building on this success, various approaches have recently been proposed for finding Pareto-optimal solutions to multi-objective MaxSAT (MO-MaxSAT) instances, i.e., propositional encodings under multiple objective functions. In this work, we propose core boosting as a reformulation/preprocessing technique for improving the runtime performance of MO-MaxSAT solvers. Core boosting in the multi-objective setting allows for shrinking the ranges of the multiple objectives at hand, which can be particularly beneficial for MO-MaxSAT relying on search that requires enforcing increasingly tighter objective bounds through propositional encodings. We show that core boosting is effective in improving the runtime performance of SAT-based MO-MaxSAT solvers with typically little overhead.

Bibtex

@inproceedings{JabsEtAl2024CoreBoostingSAT,
  author = {Jabs, Christoph and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
  booktitle = {Integration of Constraint Programming, Artificial Intelligence, and Operations Research---21th International Conference, ({CPAIOR} 2024)},
  title = {Core Boosting in SAT-Based Multi-Objective Optimization},
  year = {2024},
  editor = {Dilkina, Bistra},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
}