[Proof Complexity] MIAO seminar Wed Jan 7 at 14:00 with Andy Oertel: Certifying combinatorial optimization: A unified approach using pseudo-Boolean reasoning

[Jakob Nordström]

Dear all,

It is our great pleasure to start off the spring 2026 season of the MIAO seminar series on Wednesday January 7 at 14:00 with a presentation by our very own Andy Oertel, who will give a talk titled "Certifying combinatorial optimization: A unified approach using pseudo-Boolean reasoning". You find the abstract at the bottom of this message.

The first half of this seminar will be a general overview of certifying algorithms and proof logging, and will double as the "half-year seminar" in preparation for Andy's PhD defence. After the break, the second part of the seminar will get more technical.

We will run this as a MIAO hybrid seminar at Lund University. Local participants are warmly welcome to seminar room E:2405 at Ole Römers väg 3, while other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk<mailto:jn at di.ku.dk>.

Best regards,
Jakob Nordström

**********

Wednesday Jan 7 at 14:00 in seminar room E:2405, Ole Römers väg 3, Lund University, and on Zoom
Certifying combinatorial optimization: A unified approach using pseudo-Boolean reasoning
(Andy Oertel, Lund University and University of Copenhagen)

Combinatorial optimization is a powerful way to solve complex problems, like planning, scheduling, or even hardware verification, by expressing the problem in a mathematical form 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 allocate organs for transplantation.

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 does not increase our trust in the correctness of the answer. 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 largely infeasible for modern solvers. We propose the technique of certifying algorithms, which has been proven to be effective in providing correctness guarantees for solver outputs. The idea behind certifying algorithms is that the algorithm generates a certificate that shows the correctness of result. An independent tool can then verify that the result is correct with respect to the input using the certificate to simplify the verification effort. This verification tool can be simple enough to allow formal verification, ensuring that its verdict can be trusted.

This thesis presents a multipurpose certification system built on so-called pseudo-Boolean reasoning, which enables the generation of correctness certificates across a wide range of combinatorial optimization 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 check the correctness of the certificates, we provide a formally verified checking toolchain. Furthermore, we develop certification methods for solving paradigms that previously lacked any certifying algorithms.

In the first hour of this seminar, I will give a broad overview over the field of certifying algorithms, our certification approach, and the main contributions of my PhD thesis. In the second hour, we will have a closer look at how our certification system works and what a certificate generated by a solver looks like. We will also briefly discuss how such certificates are checked by looking at how our VeriPB checker works.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se