Faculty of Engineering, LTH

Denna sida på svenska This page in English

Digit@LTH: Events

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


From: 2022-06-10 14:15 to 17:00
Place: E:A, E-building, John Ericssons väg 2 / Ole Römers väg 3, Lund, Sweden and Online
Contact: jakob [dot] nordstrom [at] cs [dot] lth [dot] se
Save event to your calendar

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

Author: Stephan Gocht, Department of Computer Science, Lund University

Faculty opponent: Professor Marijn Heule, Carnegie Mellon University, USA.

Examination Committee:

  • Professor Elina Rönnberg, Linköping University

  • Professor Philipp Rümmer, Uppsala University

  • Professor Dmitriy Traytel, Copenhagen University

  • Deputy: Associate Professor Carl Olsson, Lund University

Session chair: Professor Volker Kreuger, Lund University

Location: E:A, E-building, John Ericssons väg 2 / Ole Römers väg 3, Lund, Sweden and Online (please register to get link)

For download: Here


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.


The event is open to anyone interested via the zoom platform. Please register to get the link: