Andy Oertel's Licentiate Seminar

• Thesis title: Certifying Combinatorial Optimization Using Pseudo-Boolean Reasoning
• Author: Andy Oertel, Department of Computer Science, Lund University
• Faculty opponent: Associate Professor Marco Chiarandini, University of Southern Denmark
• Examiner: Professor Jacek Malec, LTH
• Supervisor: Professor Jakob Nordström, LTH
• Co-supervisor: Assistant Professor Susanna de Rezende, LTH
• Date and time: Friday 28 November at 13:30
• Location: E:1406, E-huset, LTH, Klas Anshelms väg 10/Ole Römers väg 3, Lund
• A link to download the thesis will be added later

Abstract

Combinatorial optimization provides a powerful framework for solving complex optimization problems with general-purpose solvers by modelling the problem in an abstract language. Due to breakthroughs in algorithms to solve combinatorial optimization problems in last decades, combinatorial optimization has become a valid approach to solve many real world problems efficiently. Key application areas are planning, scheduling, computer-aided design, verification, and even theorem proving. However, the efficiency of the tools to solve these problems comes at the cost of increased complexity of the solvers. This makes it difficult to trust that the result computed by a combinatorial optimization solver is correct, which especially becomes a concern if the correctness of the result is mission-critical.

The main approach to address this issue is certifying algorithms, where an algorithm has to also generate a certificate that its result is correct, which can then be checked independently. This thesis demonstrates how pseudo-Boolean reasoning can be used to provide efficient certification of results returned by different kinds of combinatorial optimization solvers. We present a unified multipurpose certification system with a formally verified end-to-end verification toolchain, which guarantees that the combinatorial optimization problem was solved correctly. Developing a multipurpose certification system distinguishes this work from any prior work, which predominantly focused on very specialized approaches. We also present certification for many algorithms which, prior to our work, lacked any approach for certifying their result.