PhD Defence

Abstract

Many real-world problem settings, from network routing via scheduling to supply chain optimization, machine learning and bioinformatics, give rise to computationally hard optimization problems where optimal tradeoffs between multiple conflicting objectives are sought after. Finding all optimal solutions under multiple objectives requires algorithmic approaches that consider the multi-objective setting from the ground up. We consider the declarative approach for solving multi-objective optimization problems where problems are first modelled in a mathematical constraint language and then solved by a generic constraint optimizer for the language. As constraint languages, we focus on propositional logic and pseudo-Boolean constraints, giving rise to so-called multi-objective maximum satisfiability (MO-MaxSAT) and multi-objective pseudo-Boolean optimization (MO-PBO). In this thesis we propose algorithms and preprocessing techniques for MO-MaxSAT and MO-PBO, as well as proof logging for generating certificates of optimality for the results the algorithms produce. We provide open-source implementations of the proposed techniques and empirically evaluate their runtime performance. In terms of algorithms, we propose two novel algorithmic approaches, as well as adapt algorithms previously proposed for MO-MaxSAT to MO-PBO. The first proposed algorithm exploits properties of bi-objective instances to achieve efficient ordered enumeration of Pareto-optimal solutions. In developing the second algorithm we harness the single-objective implicit hitting set MaxSAT algorithm for enumerating optimal solutions under multiple objectives. Orthogonally to practical algorithms, we lift preprocessing techniques from Boolean satisfiability (SAT) and single-objective MaxSAT to MO-MaxSAT and propose a novel preprocessing technique that shrinks the multi-objective search space via single-objective core-guided search. For improving the trustworthiness of multi-objective optimization solvers, we enable for the first time machine-checkable certificates of optimality for the results of MO-MaxSAT and MO-PBO solvers. We detail how certificates of Pareto optimality can be generated by adapting proof logging—a concept popularized in SAT solving—in a proof format based on pseudo-Boolean constraints. The key contributions of this thesis—algorithms, preprocessing, and certificates of optimality—are implemented in an open-source solver. The practical utility of each algorithmic technique proposed in the work is empirically assessed on benchmark instances from a diverse set of problem domains, showing that our solver outperforms competing solvers for the same task.

Bibtex

@phdthesis{Jabs2026AdvancesSATBasedMultiObjective,
  author = {Jabs, Christoph},
  title = {Advances to SAT-Based Multi-Objective Constraint Optimization},
  school = {University of Helsinki},
  year = {2026},
  handle = {10138/636637},
  isbn = {78-952-84-3248-7},
  month = sep,
}