License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2023.18
URN: urn:nbn:de:0030-drops-190553
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19055/
Jabs, Christoph ;
Berg, Jeremias ;
Ihalainen, Hannes ;
Järvisalo, Matti
Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization
Abstract
Building on Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solving algorithms, several approaches to computing Pareto-optimal MaxSAT solutions under multiple objectives have been recently proposed. However, preprocessing in (Max)SAT-based multi-objective optimization remains so-far unexplored. Generalizing clause redundancy to the multi-objective setting, we establish provably-correct liftings of MaxSAT preprocessing techniques for multi-objective MaxSAT in terms of computing Pareto-optimal solutions. We also establish preservation of Pareto-MCSes - the multi-objective lifting of minimal correction sets tightly connected to optimal MaxSAT solutions - as a distinguishing feature between different redundancy notions in the multi-objective setting. Furthermore, we provide a first empirical evaluation of the effect of preprocessing on instance sizes and multi-objective MaxSAT solvers.
BibTeX - Entry
@InProceedings{jabs_et_al:LIPIcs.CP.2023.18,
author = {Jabs, Christoph and Berg, Jeremias and Ihalainen, Hannes and J\"{a}rvisalo, Matti},
title = {{Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization}},
booktitle = {29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-300-3},
ISSN = {1868-8969},
year = {2023},
volume = {280},
editor = {Yap, Roland H. C.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19055},
URN = {urn:nbn:de:0030-drops-190553},
doi = {10.4230/LIPIcs.CP.2023.18},
annote = {Keywords: maximum satisfiability, multi-objective combinatorial optimization, preprocessing, redundancy}
}
