Links
Abstract
The declarative approach is key to efficiently finding optimal solutions to various types of NP-hard real-world combinatorial optimization problems. Most work on practical declarative solvers—ranging from classical integer programming to finite-domain constraint optimization and maximum satisfiability (MaxSAT)—has focused on optimization under a single objective; fewer advances have been made towards efficient declarative techniques for multi-objective optimization problems. Motivated by significant recent advances in practical solvers for MaxSAT, in this work we develop BiOptSat, an exact declarative approach for finding Pareto-optimal solutions to bi-objective optimization problems, with propositional logic as the underlying constraint language. BiOptSat can be viewed as an instantiation of the lexicographic method. The approach makes use of a single Boolean satisfiability solver that is incrementally employed throughout the entire search procedure, allowing for finding a single Pareto-optimal solution, finding one representative solution for each non-dominated point, and enumerating all Pareto-optimal solutions. We detail several algorithmic instantiations of BiOptSat, each building on recent algorithms proposed for single-objective MaxSAT. We empirically evaluate the instantiations compared to recently-proposed alternative approaches to multi-objective MaxSAT solving on several real-world domains from the literature, showing the practical benefits of our approach.
Bibtex
@article{JabsEtAl2024FromSingleObjective, author = {Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J{\"{a}}rvisalo, Matti}, title = {From Single-Objective to Bi-Objective Maximum Satisfiability Solving}, journal = {Journal of Artificial Intelligence Research}, year = {2024}, volume = {80}, month = aug, pages = {1223--1269}, publisher = {AI Access Foundation}, url = {http://dx.doi.org/10.1613/jair.1.15333}, doi = {10.1613/jair.1.15333}, }