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

@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},
}