MIAO seminar Mon Nov 28 at 14:00 CET: Combinatorial solving with provably correct results
7 views
Skip to first unread message
Jakob Nordström
Nov 4, 2022, 4:49:54 PM11/4/22
to Constraint solving mailing list
Dear all,
Combinatorial solving algorithms for NP-hard problems have made astounding progress over the last couple of decades, but still struggle with a very 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 this problem can be addressed in a principled way using *proof* *logging*, meaning that solvers output not only a result but also a simple, machine-verifiable proof that this result has been computed correctly. This has already been used for quite some time in the Boolean satisfiability (SAT) community, and research progress in the last few years now seem to hold out the promise of similar tools 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
Combinatorial solving algorithms for NP-hard problems have made astounding progress over the last couple of decades, but still struggle with a very 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 this problem can be addressed in a principled way using *proof* *logging*, meaning that solvers output not only a result but also a simple, machine-verifiable proof that this result has been computed correctly. This has already been used for quite some time in the Boolean satisfiability (SAT) community, and research progress in the last few years now seem to hold out the promise of similar tools 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
Reply all
Reply to author
Forward
0 new messages