[Proof Complexity] MIAO seminar Mon Nov 28 at 14:00 CET: Combinatorial solving with provably correct results

[Jakob Nordström]

Dear proof complexity colleagues,

Despite all our efforts at proving strong lower bounds, astounding progress on combinatorial solving algorithms over the last couple of decades means that practitioners nowadays solve huge instances of NP-hard problems very efficiently. Except that they still struggle with a quite fundamental question: How can we be sure that the results computed are correct? In fact, we know we *cannot* be sure about this --- even the most mature commercial solvers are known to sometimes produce buggy results.

On Monday November 28 at 14:00 CET we will have a ca-2-hour video tutorial on how proof complexity can be leveraged to solve this problem. By requiring solvers to use use *proof* *logging*, meaning that they should output not only a result but also a simple, machine-verifiable proof that this result has been computed correctly, the task of verifying correctness can be delegated to a simple, stand-alone proof checker. This approach has been used with great success in the Boolean satisfiability (SAT) community, using, essentially, the extended resolution proof system for proof logging. We will try to explain how shifting instad to cutting planes with appropriate extension rules seems to hold out the promise of similarly efficient proof logging support for constraint programming, MaxSAT solving, 0-1 integer linear programming, and other combinatorial optimization paradigms.

You find the abstract for the tutorial at the bottom of this message. We will meet on Zoom at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested (but please do not publish the meeting link online). We are also hoping to record the tutorial and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about upcoming MIAO seminars can be found at http://www.jakobnordstrom.se/miao-seminars/ .

Best regards,
Jakob Nordström

**********

Monday Nov 28 at 14:00 on Zoom
Combinatorial solving with provably correct results
(Bart Bogaerts, Vrije Universiteit Brussel; Ciaran McCreesh, University of Glasgow; and Jakob Nordström, University of Copenhagen and Lund University)

Modern combinatorial optimization has had a major impact in science and industry, but there is a quite poor scientific understanding how state-of-the-art algorithms, so-called combinatorial solvers, work. More importantly, even mature commercial solvers are known to sometimes produce wrong results, which can be fatal for some types of applications.

One way to address this problem is to enhance combinatorial solvers with proof logging, meaning that they output not only a result but also a proof of correctness. One can then feed the problem, result, and proof to a dedicated proof checker to verify that there are no errors. Crucially, such proofs should require low overhead to generate and be easy to check, but should supply 100% guarantees of correctness.

In this tutorial, we will survey recent progress on proof logging techniques for Boolean satisfiability (SAT) solving, pseudo-Boolean optimization, and constraint programming. We will argue that moving from the clausal format employed in SAT proof logging to so-called pseudo-Boolean reasoning using 0-1 integer linear constraints seems to hit a sweet spot between on the one hand making proofs simple and easy to verify and on the other hand providing sufficient expressive power to support the sophisticated reasoning in more general combinatorial optimization paradigms.


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