Material regarding my presentation @ CPAIOR’24 about Core Boosting in SAT-Based Multi-Objective Optimization.
Links
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}, }