CP'23 - Preprocessing for Multi-Objective MaxSAT

Material regarding my presentation @ CP’23 about Preprocessing for SAT-Based Multi-Objective Combinatorial Optimization.

  1. 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.


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