Arrow Research search
Back to SAT

SAT 2022

SAT-Based Leximax Optimisation Algorithms

Conference Paper Accepted Paper Logic in Computer Science · Satisfiability

Abstract

In several real-world problems, it is often the case that the goal is to optimise several objective functions. However, usually there is not a single optimal objective vector. Instead, there are many optimal objective vectors known as Pareto-optima. Finding all Pareto-optima is computationally expensive and the number of Pareto-optima can be too large for a user to analyse. A compromise can be made by defining an optimisation criterion that integrates all objective functions. In this paper we propose several SAT-based algorithms to solve multi-objective optimisation problems using the leximax criterion. The leximax criterion is used to obtain a Pareto-optimal solution with a small trade-off between the objective functions, which is suitable in problems where there is an absence of priorities between the objective functions. Experimental results on the Multi-Objective Package Upgradeability Optimisation problem show that the SAT-based algorithms are able to outperform the Integer Linear Programming (ILP) approach when using non-commercial ILP solvers. Additionally, experimental results on selected instances from the MaxSAT evaluation adapted to the multi-objective domain show that our approach outperforms the ILP approach using commercial solvers.

Authors

Keywords

  • Multi-Objective Optimisation
  • Leximax
  • Sorting Networks

Context

Venue
International Conference on Theory and Applications of Satisfiability Testing
Archive span
2003-2025
Indexed papers
824
Paper id
943897688474841363
v2026.09.13