[Proof Complexity] PhD defence by Stephan Gocht Fri Jun 10 at 14:15

[Jakob Nordström]

[Apologies for any multiple postings]

Dear all,

It is an immense pleasure to announce that on Friday June 10 at 14:15 CET Stephan Gocht will defend his PhD thesis "Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning". You find the abstract below, and the full thesis is available at https://portal.research.lu.se/sv/publications/certifying-correctness-for-combinatorial-algorithms-by-using-pseu .

The PhD defence will take place in Lecture Hall E:A in building E at Ole Römers väg 3 at Lund University, but will also be possible to follow on Zoom at https://lu-se.zoom.us/j/65063539541?pwd=TTRoNmhtTWdGRE0zams0a3RWWDJWZz09 .

Best regards,
Jakob Nordström


ABSTRACT

Over the last decades, dramatic improvements in combinatorial optimisation algorithms have significantly impacted artificial intelligence, operations research, and other areas. These advances, however, are achieved through highly sophisticated algorithms that are difficult to verify and prone to implementation errors that can cause incorrect results. A promising approach to detect wrong results is to use certifying algorithms that produce not only the desired output but also a certificate or proof of correctness of the output. An external tool can then verify the proof to determine that the given answer is valid. In the Boolean satisfiability (SAT) community, this concept is well established in the form of proof logging, which has become the standard solution for generating trustworthy outputs. The problem is that there are still some SAT solving techniques for which proof logging is challenging and not yet used in practice. Additionally, there are many formalisms more expressive than SAT, such as constraint programming, various graph problems and maximum satisfiability (MaxSAT), for which efficient proof logging is out of reach for state-of-the-art techniques.

This work develops a new proof system building on the cutting planes proof system and operating on pseudo-Boolean constraints (0-1 linear inequalities). We explain how such machine-verifiable proofs can be created for various problems, including parity reasoning, symmetry and dominance breaking, constraint programming, subgraph isomorphism and maximum common subgraph problems, and pseudo-Boolean problems. We implement and evaluate the resulting algorithms and a verifier for the proof format, demonstrating that the approach is practical for a wide range of problems. We are optimistic that the proposed proof system is suitable for designing certifying variants of algorithms in pseudo-Boolean optimisation, MaxSAT and beyond.


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