New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization

TL;DR

This paper introduces two novel unsatisfiability-based algorithms for multi-objective combinatorial optimization, leveraging SAT solvers to improve performance over existing methods in solving complex multi-objective problems.

Contribution

The paper presents the first core-guided and hitting set-based MOCO algorithms that utilize SAT solvers, advancing the state of the art in multi-objective optimization.

Findings

Our algorithms outperform existing SAT-based MOCO methods on benchmark instances.

Experimental results demonstrate improved efficiency and solution quality.

The new methods effectively handle complex multi-objective problems.

Abstract

In the last decade, a plethora of algorithms for single-objective Boolean optimization has been proposed that rely on the iterative usage of a highly effective Propositional Satisfiability (SAT) solver. But the use of SAT solvers in Multi-Objective Combinatorial Optimization (MOCO) algorithms is still scarce. Due to this shortage of efficient tools for MOCO, many real-world applications formulated as multi-objective are simplified to single-objective, using either a linear combination or a lexicographic ordering of the objective functions to optimize. In this paper, we extend the state of the art of MOCO solvers with two novel unsatisfiability-based algorithms. The first is a core-guided MOCO solver. The second is a hitting set-based MOCO solver. Experimental results obtained in a wide range of benchmark instances show that our new unsatisfiability-based algorithms can outperform state-of-the-art SAT-based algorithms for MOCO.