Combinatorial Solving with Provably Correct Results

VeriPB Tutorial Series

About

In this tutorial series, we introduce the wonderful world of certified algorithms for combinatorial optimization, also known as proof logging. We have delivered different versions of this tutorial at various occasions. The slides of each of these iterations are available online; in chronological order:

Getting Started

Convinced by the potential of proof logging? Try it out yourself! You can download VeriPB here. For most examples in our tutorial, the original problem specification, the VeriPB proof, and instructions on how to run them can be found below:

Abstract

Combinatorial optimization problems are ubiquitous in our lives. They show up in the forms of matching problems (e.g., assigning junior doctors to hospitals), scheduling problems (e.g., radiation therapy), logistics problems (e.g., visiting nurses), and many more. In many cases, these problems are also notoriously hard (often NP-hard, or even worse). Still, thanks to tremendous progress over the last decades, we now have access to sophisticated algorithms that can solve these problems in practice. Unfortunately, it turns out that, due to their immense complexity, these (solving) algorithms often contain subtle bugs. In this tutorial, we give an overview of the most successful approach to dealing with this issue, namely proof logging, meaning that solvers aren't allowed to just claim an answer to a problem: they're expected to also produce an independently verifiable proof that backs up this claim. In the field of Boolean Satisfiability, this has done wonders for solver reliability, and has also helped with social acceptability of computer-generated mathematical results. What if we could do the same for the more general field of constraint programming, producing an auditable solving process where people whose lives or livelihoods are affected by a computer's decision would no longer have to resort to hoping that the system is free of bugs?

We will start this tutorial by explaining what a proof really is, and what it means for an algorithm to certify the correctness of its answers by using proof logging. We will give a brief overview of the (extended) resolution and DRAT proof systems used in SAT proof logging. Then we will look at what is needed to bring proof logging to a broader range of solving algorithms, starting with some subgraph-finding algorithms, and moving towards a full CP solver with multiple global constraints and even some reformulation. We will show, by example, what you need to do to use this technology in your own algorithms, and how this relates to the underlying proof methods. We'll finish by discussing how proof logging can also support advanced solving techniques such as symmetry breaking. Surprisingly, all of this can be done in a simple proof format known as "cutting planes with strengthening" that does not know anything about non-binary variables, global constraints, graphs, groups, or symmetries.

Speakers

Bart Bogaerts

Artificial Intelligence Lab
Vrije Universiteit Brussel

Ciaran McCreesh

Formal Analysis, Theory and Algorithms group
University of Glasgow

Jakob Nordström

Department of Computer Science
University of Copenhagen
and Lund University