Material regarding my presentation @ CP’23 about Preprocessing for SAT-Based Multi-Objective Combinatorial Optimization.
Links
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
@inproceedings{JabsEtAl2023PreprocessingSATBased, author = {Jabs, Christoph and Berg, Jeremias and Ihalainen, Hannes and J{\"{a}}rvisalo, Matti}, booktitle = {29th International Conference on Principles and Practices of Constraint Programming ({CP} 2023)}, title = {Preprocessing in {SAT}-Based Multi-Objective Combinatorial Optimization}, year = {2023}, editor = {Yap, Roland H. C.}, pages = {18:1--18:19}, publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik}, series = {Leibniz International Proceedings in Informatics ({LIPIcs})}, volume = {280}, doi = {10.4230/LIPIcs.CP.2023.18}, annote = {Keywords: maximum satisfiability, multi-objective combinatorial optimization, preprocessing, redundancy}, }