[Proof Complexity] MIAO seminar today Wed Jan 7 and proof complexity lectures Thu Jan 8 and Fri Jan 9

[Jakob Nordström]

Dear all,

Here comes a reminder that the spring 2026 season of the MIAO seminar series is starting today *Wednesday January 7 at 14:00 CET *with *Andy Oertel's talk "Certifying combinatorial optimization: A unified approach using pseudo-Boolean reasoning"* (abstract at the bottom of this message).

We will run this as a MIAO hybrid seminar, with local participants welcome to Lund University and others equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 .

On *Thursday January 8 at 13:15 CET *we will then resume our course / lecture series *"Proof Complexity as a Computational Lens"* (https://jakobnordstrom.se/teaching/proofcplx25/). We will talk about some deeply intriguing results on /total space in resolution and monomial space in polynomial calculus/, featuring breakthrough results by Bonacina and by Galesi, Kołodziejczyk, & Thapen, and with the lecture streamed via the same meeting room https://lu-se.zoom.us/j/61925271827 . On *Friday January 9 at 13:15 CET *we will have another proof complexity lecture on /size-degree trade-offs in algebraic proof systems (and size-width trade-offs in resolution)/, building on works by de Rezende et al., Thapen, and Lagarde et al.

Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record both the seminar and the lectures and post them on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the presentations 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.

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