2026-07-25T23:08:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19055 2024-03-06T11:03:23Z ddc:004 open_access

Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization Jabs, Christoph Berg, Jeremias Ihalainen, Hannes Järvisalo, Matti maximum satisfiability multi-objective combinatorial optimization preprocessing redundancy 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Jabs and Jeremias Berg and Hannes Ihalainen and Matti Järvisalo 2023 Is Part Of LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2023.18 urn:nbn:de:0030-drops-190553 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.18 eng https://creativecommons.org/licenses/by/4.0/legalcode