[Proof Complexity] Seminar Wed Jun 1 at 14:00 CET with Stephan Gocht: Certifying correctness for combinatorial algorithms by using pseudo-Boolean reasoning

[Jakob Nordström]

Dear all,


On Wednesday June 1 at 14:00 CET we are having a seminar with Stephan Gocht from Lund University and the University of Copenhagen titled "Certifying correctness for combinatorial algorithms by using pseudo-Boolean reasoning". In this seminar, Stephan will present some of the award-winning work done during his PhD project, and also demonstrate how the methods he has developed can be used in practice. You find the abstract at the bottom of this message.

We will run this as a hybrid seminar at the University of Copenhagen. Local participants are welcome on UCPH campus --- the exact location will be communicated later. Other participants are still 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://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)


More information about upcoming MIAO seminars can be found at http://www.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 Jun 1 at 14:00 at the University of Copenhagen and on Zoom
Certifying correctness for combinatorial algorithms by using pseudo-Boolean reasoning
(Stephan Gocht, Lund University and University of Copenhagen)

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, we 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 I developed during my PhD project.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se