Core Boosting in SAT-Based Multi-objective Optimization

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---21st International Conference, {CPAIOR} 2024, Uppsala, Sweden, May 28--31, 2024, Proceedings, Part {II}},
  title = {Core Boosting in SAT-Based Multi-objective Optimization},
  year = {2024},
  editor = {Dilkina, Bistra},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  pages = {1--19},
  volume = {14743},
  isbn = {978-3-031-60599-4},
  doi = {10.1007/978-3-031-60599-4_1},
  url = {https://link.springer.com/chapter/10.1007/978-3-031-60599-4_1},
}