Andy Oertel's PhD defence

Thesis title: Certifying Combinatorial Optimization: A Unified Approach Using Pseudo-Boolean Reasoning”

Author: Andy Oertel, Department of Computer Science, Lund University

Faculty opponent: Professor Emeritus Randal Bryant, Carnegie Mellon University, USA

Examination Committee:

• Professor Erika Ábrahám, RWTH Aachen, Germany
• Associate Professor Justin Pearson, Uppsala University
• Associate Professor Monika Seisenberger, Swansea University, The United Kingdom
• Deputy: Associate Professor Paul Stankovski Wagner, Lund University

Session chair: Professor Görel Hedin, Lund University

Supervisors:

• Main supervisor: Professor Jakob Nordström, Lund University
• Associate Senior Lecturer Susanna Rezende, Lund University

Location: E:1406, E-huset, Klas Anshelms väg 10/Ole Römers väg 3, Lund

Here is a link to download the thesis at LU Research Portal

Abstract

Combinatorial optimization is a powerful way to solve complex problems, like planning, scheduling, or hardware verification, by expressing the problem in a mathematical form using discrete variables that can be solved by general solvers. Due to major advances in algorithms for solving combinatorial optimization problems, these solvers can tackle real-world challenges efficiently. However, as solvers become more powerful, they also become larger and more complex, which makes it harder to trust that their output is correct. Ensuring that the solver gives a correct answer becomes especially important when mistakes could have serious consequences, e.g., when solvers are used to match organ donors and recipients or dispatch ambulances.

Testing the solver, which verifies correctness only on known input-output pairs, provides no guarantee that the solver returns correct answers on untested inputs and therefore we can not fully trust that the answer is correct. Formal verification can prove that a solver adheres to a formal specification and thus guarantees that the answer of the solver is correct, but this approach remains infeasible for modern solvers. The approach that has proven most effective for providing correctness guarantees for solver outputs is certifying algorithms. The idea behind certifying algorithms is that the algorithm generates a certificate that shows the correctness of the result. An independent tool can then use the certificate to verify that the result is correct with respect to the input. This verification tool can be simple enough to enable formal verification of its correctness, ensuring that its verdict can be trusted.

This thesis presents the first viable certification approach for several combinatorial optimization solvers that had previously been considered out of reach. This is achieved through a multipurpose certification system built on so-called pseudo-Boolean reasoning, which enables the generation of correctness certificates across a these wide range of different solver paradigms. Developing a multipurpose system allows the checker to be reused for all types of solvers, which sets our work apart from previous, more specialized approaches. Although we use pseudo-Boolean reasoning to certify the solver output, the solver itself does not need to perform pseudo-Boolean reasoning, and making a solver certifying does not require any changes to its internal reasoning. To have also developed a checker that is formally verified to be correct to ensure that this checker can be truster.