  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.
