Engineering and Evaluating Multi-objective Pseudo-Boolean Optimizers
摘要
Various real-world settings give rise to combinatorial optimization problems with multiple conflicting objectives, motivating the development of practical approaches to the challenging task of finding Pareto-optimal solutions to declarative models of multi-objective problems. In this work we focus on multi-objective optimization over pseudo-Boolean constraints (MO-PBO) as an extension of propositional clauses and, at the same time, an important class of 0–1 linear constraints. We provide a first-of-kind cross-community evaluation of a selection of recently-proposed approaches applicable to MO-PBO, including first implementations of native MO-PBO algorithms we provide as well as approaches based on integer linear programming techniques and a translation-based approach to MO-MaxSAT, providing insights into the current state-of-the-art approaches to MO-PBO. In terms of algorithmic advances, we engineer MO-PBO solvers by harnessing recent advances in decision procedures for pseudo-Boolean constraints in order to lift multi-objective approaches recently developed for multi-objective optimization under propositional constraints (i.e., MO-MaxSAT) to the realm of MO-PBO. Extending on recent work on certified MO-MaxSAT solving, we also realize certified multi-objective pseudo-Boolean optimization by implementing proof logging for both our native MO-PBO approach and the translation-based MO-MaxSAT approach.