Jakob Nordström / WHOOPS '24

1st International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '24)

Background

Since the turn of the millennium there have been dramatic improvements in algorithms for combinatorial solving and optimization. The flipside of this is that as the methods get increasingly sophisticated, it becomes increasingly harder to avoid bugs sneaking in during algorithm design and implementation, and it is well documented that even the most mature tools currently available sometimes return incorrect results. Software testing, while important, has not been sufficient to resolve this problem, and formal verification methods are far from being able to scale to the level of complexity in modern combinatorial solvers. During the last ten years the Boolean satisfiability (SAT) solving community has instead successfully introduced proof logging, meaning that the SAT solvers have to output, along the answer to a problem, a machine-verifiable proof that this answer is correct. Such solvers are also referred to as certifying algorithms.

For a long time, attempts to extend proof logging to stronger algorithmic paradigms such as SAT-based optimization (MaxSAT), constraint programming, and mixed integer linear programming have met with very limited success. This has changed in the last few years with the introduction of pseudo-Boolean (PB) proof logging. Pseudo-Boolean proofs operate with 0-1 integer linear inequalities using a version of the cutting planes proof system, but have turned out to be a very convenient format also for algorithms that reason in terms of very different concepts. The VeriPB tool developed by the Mathematical Insights into Algorithms for Optimization (MIAO) research group in Copenhagen/Lund and its collaborators has so far been shown to support efficient proof logging not only for advanced SAT solving techniques previously beyond reach (including symmetry breaking), but also for MaxSAT solving, subgraph solving, constraint programming, and presolving techniques in 0-1 integer linear programming.

These developments have been so fast that the (somewhat spontaneous) idea has arisen to gather researchers from all over Europe working on pseudo-Boolean proof logging during the week May 20-24 in Copenhagen. The intention is to have an informal workshop where the attendees can learn about the latest news, hear about work that is ongoing right now, do networking, and plan for future collaborations. Reflecting the rather improvised nature of this event, it has been named the 1st Workshop on Highlights in Organizing and Optimizing Proof-logging Systems, or WHOOPS '24 for short.

Program

During the first half of the week, we will have informal research discussions interleaved with a couple of longer seminars on Tuesday and Wednesday as listed separately on the MIAO seminar webpage.

On Thursday-Friday we will have a workshop dedicated to proof logging with scheduled talks as listed below. The workshop will be held in seminar room N116A&B at Universitetsparken 1 at the Department of Computer Science (DIKU) at the University of Copenhagen. We will also try to stream most of the presentations over Zoom. Please contact Jakob Nordström if you would be interested in participating in the workshop (virtually or on site).

Please note that most of the titles in the schedule below are still provisional.

THURSDAY MAY 23
09:45-10:00 Welcome and presentation of participants
10:00-11:00 A one-size-fits-all proof logging system? Jakob Nordström
11:00-12:00 Symmetry and dominance breaking using pseudo-Boolean proof logging Bart Bogaerts
12:00-13:30 Lunch
13:30-14:30 Pseudo-Boolean proof logging for things that don't look pseudo-Boolean Ciaran McCreesh
14:30-15:30 Recent advances in proof logging for constraint programming Matthew McIlree
15:30-16:00 Break
16:00-17:00 Proof logging for maximum satisfiability (MaxSAT) solving Dieter Vandersande
17:00-18:00 Pitches and discussions about future directions and feature requests
18:15 Leave for workshop dinner at Madklubben Østerbro at Østerbrogade 79
 
FRIDAY MAY 24
10:00-11:00 Proof logging for MaxSAT preprocessing Hannes Ihalainen
11:00-11:30 Break
11:30-12:00 Proof logging for presolving in 0-1 integer linear programming Andy Oertel
12:00-12:30 Handling symmetries in subgraph finding Joe Loughney
12:30-13:00 Pseudo-Boolean proof trimming Arthur Gontier
13:00 Lunch and end of formal workshop

About the MIAO Research Group

The Mathematical Insights into Algorithms for Optimization (MIAO) research group is based on both sides of the Øresund Bridge at the University of Copenhagen and Lund University. The group has a unique profile in that we are doing cutting-edge research both on the mathematical foundations of efficient computation and on state-of-the-art practical algorithms for real-world problems. This creates a very special environment, where we do not only conduct in-depth research on different theoretical and applied topics, but where different lines of research cross-fertilise each other and unexpected and exciting synergies often arise.

We are closely affiliated with the Basic Algorithms Research Copenhagen (BARC) centre, and are part of a world-leading environment in algorithms and complexity theory encompassing also the IT University of Copenhagen and the Technical University of Denmark (DTU). We aim to attract top talent from around the world to an ambitious, creative, collaborative, and fun environment. Using the power of mathematics, we strive to create fundamental breakthroughs in algorithms and complexity theory. While the focus in on foundational research, algorithms and complexity researchers in Copenhagen have a track record of surprising algorithmic discoveries leading to major industrial applications.

Published by: Jakob Nordström <jn~at-sign~di~dot~ku~dot~dk>
Updated 2024-05-14