BARC/MIAO talk by Stephan Gocht

Wednesday, 1 June 2022, Stephan Gocht, PhD student at Lund University, Sweden, will give a talk on "Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning".

Title:
Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning

Abstract:
Although solving NP-complete problems is widely believed to require exponential time in the worst case, state-of-the-art  algorithms are amazingly efficient for many NP-hard optimisation problems. However, this is achieved through highly sophisticated algorithms that are prone to implementation errors which can cause incorrect results, even for the best commercial tools. A promising approach to address this problem is to use certifying algorithms that produce not only the desired output but also a simple, machine verifiable certificate or proof of correctness of the output. By verifying this proof with an external tool, we can guarantee that the given answer is valid.

This talk gives an introduction to a new proof system that can certify answers of algorithms for various combinatorial problems, such as Boolean satisfiability (SAT) solving and optimisation, constraint programming, and graph solving. This proof system operates on 0-1 integer linear constraints, generalising the cutting planes proof system. As a running example, Stephan will show how to certify the correctness of a maximum matching algorithm.

After the official seminar, there will be an optional second part with more technical discussions. This second part will  demonstrate how to generate such machine verifiable proofs in practice and how to check them using the verifier VeriPB, which Stephan developed during his PhD.

Bio:
Stephan Gocht is a PhD student at Lund University in the mathematical insights and algorithms for optimisation (MIAO) group and guest researcher at BARC. He recently received an AAAI distinguished paper award for his work on certifying algorithms.