AAAI-24

Combinatorial Solving with Provably Correct Results

A AAAI 2024 tutorial

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.