Jakob Nordström / WHOOPS '24

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

Follow the links to read about the background and purpose of this workshop, the workshop program with titles and abstracts of the presentations, and the MIAO research group.

Background and Purpose

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.

Workshop 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.

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	Certified symmetry breaking with VeriPB	Bart Bogaerts
12:00-13:30	Lunch
13:30-14:30	Pseudo-Boolean proof logging for things that aren't pseudo-Boolean	Ciaran McCreesh
14:30-15:30	Proof logging for some interesting constraint propagation algorithms	Matthew McIlree
15:30-16:00	Break
16:00-17:00	Proof logging for MaxCDCL and BDDs	Dieter Vandesande
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	Certified MaxSAT preprocessing	Hannes Ihalainen
11:00-11:30	Break
11:30-12:00	Certifying MIP-based presolve reductions for 0–1 integer linear programs	Andy Oertel
12:00-12:30	Symmetry breaking in the subgraph isomorphism problem	Joseph Loughney
12:30-13:00	Pseudo-Boolean proof trimming	Arthur Gontier
13:00	Lunch and end of formal workshop

Titles and Abstracts of Presentations

Jakob Nordström: A one-size-fits-all proof logging system?

This talk is intended to give an overview of VeriPB, a proof system based on pseudo-Boolean reasoning with 0-1 integer linear inequalities that seems well suited to provide a unified proof logging method for discrete combinatorial problems. We have implemented VeriPB proof logging, together with efficient proof checking, for state-of-the-art solvers in Boolean satisfiability (SAT) solving, SAT-based optimization (MaxSAT solving), graph solving, constraint programming, and a growing list of other combinatorial solving paradigms. We believe there are reasons to hope that ideas from VeriPB could be useful also in the context of mixed integer linear programming, satisfiability modulo theories (SMT) solving, automated planning, and possibly also other combinatorial solving paradigms, and will briefly review these and other future research directions in pseudo-Boolean proof logging.

Based on joint work with Jeremias Berg, Bart Bogaerts, Jan Elffers, Ambros Gleixner, Stephan Gocht, Alexander Hoen, Hannes Ihalainen, Matti Järvisalo, Ciaran McCreesh, Matthew McIlree, Magnus O. Myreen, Andy Oertel, Yong Kiam Tan, and Dieter Vandesande.

Bart Bogaerts: Certified symmetry breaking with VeriPB

I will start by giving an overview of (static and dynamic) symmetry handling methods for SAT. Next, I will dive into details about strengthening rules in the VeriPB proof system and discuss every step of a detailed worked example, demonstrating how to do fully automated static symmetry breaking for SAT in a certified way. Finally, I will discuss an open challenge on how to get certification for a framework such as SAT modulo symmetries, and particularly, the question of what it even means to certify this method.

Ciaran McCreesh: Pseudo-Boolean proof logging for things that aren't pseudo-Boolean

We've heard a lot about pseudo-Boolean proof logging, but what do we do if our problems aren't pseudo-Boolean and our solvers don't search for cutting planes proofs? I'll showcase a range of applications where VeriPB has been successfully deployed, including subgraph problems like maximum clique and subgraph isomorphism; constraint programming; and if time permits, dynamic programming. These results suggest that for some reason, extended cutting planes seems to be a really helpful way of certifying a wide range of techniques used in combinatorial solving algorithms.

Matthew McIlree: Proof logging for some interesting constraint propagation algorithms

In this talk, I will explain some non-trivial propagators used in constraint programming solvers, and describe how they can be modified to justify their reasoning within the VeriPB proof system.

Dieter Vandesande: Proof logging for MaxCDCL and BDDs

In earlier work, MaxSAT solvers implementing both solution-improving and core-guided search have been made certifying using the VeriPB proof system. In this talk, I will show the recent developments and ongoing work on proof logging a solver implementing a third solving paradigm: Branch-and-Bound search. More specifically, will we cover the solver MaxCDCL, which combines Branch-and-Bound search with the power of clause learning as it is implemented in SAT solvers. MaxCDCL also makes use of a PB-to-CNF encoding based on BDD's, and we will also show how to provide proof logging for that.

Hannes Ihalainen: Certified MaxSAT preprocessing

Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems. However, ensuring correctness of MaxSAT solvers has remained a considerable concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper.

In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we provide formally verified end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.

The talk is based on the work "Certified MaxSAT Preprocessing" by Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, and Jakob Nordström that appeared at IJCAR 2024.

Andy Oertel: Certifying MIP-based presolve reductions for 0–1 integer linear programs

It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the feasibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on 0-1 integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and leads to suggestions for future revisions of the proof format that will help to reduce the verbosity of the certificates and to accelerate the certification and verification process further.

Joseph Loughney: Symmetry breaking in the subgraph isomorphism problem

The Subgraph Isomorphism Problem has many applications, including bioinformatics, computer vision and graph databases. Current state-of-the-art solvers using constraints programming techniques can handle cases with up to 1000 pattern vertices and 10,000 target vertices. Symmetry breaking techniques have shown promising results in improving the efficiency of algorithms for similar combinatorial problems; presented here are two strategies for implementing symmetry breaking using stabiliser chains, alongside initial experimental results.

Arthur Gontier: Pseudo-Boolean proof trimming

Proof trimming may be used to get a smaller proof, a shorter verification time or to gain some knowledge on the solving method that generated the proof. In this talk, we will present some early results of a trimmer we made for CP proofs on Subgraph Isomorphism Problems, and we open the discussion on several trimming ideas.

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.