Andy Oertel: Certifying combinatorial optimization: A unified approach with pseudo-Boolean reasoning

Описание: Wednesday Jan 7, 2025
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.


For more information about the MIAO seminars, please visit https://jakobnordstrom.se/miao-seminars/ .