M.Sc. Christoph Jabs defends his PhD thesis “Advances to SAT-Based Multi-Objective Constraint Optimization” on Friday the 11th of September 2026 at 13 in the University of Helsinki Chemicum building, Auditorium A110 (A. I. Virtasen aukio 1, 1st floor). His opponent is Professor Daniel Le Berre (University of Artois, France) and custos Professor Matti Järvisalo (University of Helsinki). The defence will be held in English.
The thesis of Christoph Jabs is a part of research done in the Department of Computer Science and in the Constraint Reasoning and Optimization group at the University of Helsinki. His supervisors have been Professor Matti Järvisalo and Academy Research Fellow Jeremias Berg (University of Helsinki).
Advances to SAT-Based Multi-Objective Constraint Optimization
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.
Availability of the dissertation
An electronic version of the doctoral dissertation will be available in the University of Helsinki open repository Helda at
Printed copies will be available on request from Christoph Jabs: