From Single-Objective to Bi-Objective Maximum Satisfiability Solving

From Single-Objective to Bi-Objective Maximum Satisfiability Solving
2024
Journal of Artificial Intelligence Research, 2024, (accepted for publication)
  1. 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},
      pubstate = {accepted for publication},
    }