Jakob Nordström / WHOOPS '25

2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25)

Follow the links to read about the background and purpose of the WHOOPS '25 workshop, registration and travel funding, venue and online attendance, the workshop program with titles and abstracts of the presentations, and the organizers.

Executive Summary

The 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25) was held on September 13-14, 2025, at Institut Pascal in Orsay on the outskirts of Paris in coordination with the EuroProofNet Workshop on Automated Reasoning and Proof Logging, which was in turn part of the Final EuroProofNet Symposium.

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 even the most mature tools currently available struggle with 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 twenty years the Boolean satisfiability (SAT) solving community has instead spearheaded the use of 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 paradigms in combinatorial solving and optimization have met with limited success, but 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 for paradigms such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, subgraph solving, constraint programming, automated planning, and presolving techniques in 0-1 integer linear programming, as well as for techniques such as symmetry breaking and dynamic programming.

These developments have been so fast that in 2024 the fairly spontaneous idea arose to gather researchers working on pseudo-Boolean proof logging to an informal gathering, which—reflecting the rather improvised nature of the event—was named the 1st Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '24). This year, the second edition of the workshop was held on September 13-14 in Orsay outside Paris under the auspices of EuroProofNet. In addition to offering a healthy dose of pseudo-Boolean proof logging, the purpose of WHOOPS has evolved to provide a forum for discussing certifying algorithms for automated reasoning more broadly, including satisfiability modulo theories (SMT) solving and first- and higher-order theorem proving.

Registration and Travel Funding

Registration is free but mandatory. The Final EuroProofNet Symposium organizers asked for the registration form to be filled in by May 25, 2025.

As part of the registration, it was also possible to apply for travel funding from EuroProofNet. See also information about the formal eligibility rules.

Venue (and Online Attendance)

WHOOPS '25 was held at Institut Pascal at 530 Rue André Rivière, 91400 Orsay (see map).

It was also possible to attend the workshop online.

The links below provide information about local travel directions, nearby hotels, and food options.

Workshop Program

The workshop program was structured as follows:

Saturday offered a collection of slightly longer, tutorial-style, talks, explaining how pseudo-Boolean proof logging can support efficient certified solving for paradigms such as SAT solving, SAT-based optimization (MaxSAT), pseudo-Boolean optimization, subgraph solving, and constraint programming.
On Sunday we had contributed talks, presenting some of the very latest news in pseudo-Boolean proof logging, but also discussing other proof logging techniques as well as problems for which no efficient proof logging currently exists.

SATURDAY SEPTEMBER 13
09:00-10:00	An introduction to pseudo-Boolean proof logging	Jakob Nordström
10:00-11:00	Proof logging for subgraph solving	Ciaran McCreesh
11:00-11:30	Morning break (with presentation round for participants)
11:30-12:30	Proof logging for constraint programming	Matthew McIlree
12:30-14:00	Lunch (arrange on your own)
14:00-15:00	Proof logging for pseudo-Boolean optimization	Wietze Koops
15:00-15:30	Afternoon break
15:30-16:30	Proof logging for preprocessing/presolving in MaxSAT and 0-1 integer linear programming	Andy Oertel
16:30-17:30	Proof logging for symmetry breaking	Markus Anders
17:30-18:30	Time for discussion about the past, present and future of proof logging
19:00	Improvised workshop dinner

SUNDAY SEPTEMBER 14
09:00-09:30	End-to-end verification for subgraph solving [demo]	Yong Kiam Tan (remote)
09:30-10:00	A variety of trimming techniques for pseudo-Boolean proof logs	Arthur Gontier
10:00-10:30	Pseudo-Boolean proof logging for optimal classical planning	Simon Dold
10:30-11:00	Short, composable proofs without interference	Adrian Rebola-Pardo
11:00-11:30	Morning break
11:30-12:00	Proof Logging in CaDiCaL	Florian Pollitt
12:00-12:30	Symmetry breaking in the subgraph isomorphism problem	Ruth Hoffmann
12:30-14:00	Lunch (arrange on your own, possibly in advance—see above)
14:00-14:30	Formal verification for constraint solvers	Catherine Dubois
14:30-15:00	Wishes for the VeriPB proof format: An update	Daniel Le Berre
15:00	End of workshop

Titles and Abstracts of Presentations

An introduction to pseudo-Boolean proof logging (Jakob Nordström, University of Copenhagen and Lund University)

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 a wide range of problems in discrete combinatorial solving and optimization.

Proof logging for subgraph solving (Ciaran McCreesh, University of Glasgow)

Many interesting problems involve finding a little graph inside a bigger graph: for example, maximum clique asks for the largest set of vertices where everything is adjacent, whilst subgraph isomorphism asks whether a specific pattern occurs inside a given target graph. Although these problems are computationally hard in theory, in practice solvers can often handle these problems extremely quickly, even on graphs with thousands of vertices. However, these solvers are not always perfect, and sometimes contain bugs that lead to wrong answers being produced. I'll explain how, using the VeriPB proof system, we can augment these solvers to produce correctness certificates, allowing us to be confident they have definitely given the right answers. To do this, we'll need to be able to justify a wide range of algorithmic inference steps, including colour bounds, all-different filtering, and degree reasoning; perhaps surprisingly, VeriPB is able to do all of these efficiently, despite not having any notion of what a graph is.

Pseudo-Boolean proof logging for constraint programming (Matthew McIlree, University of Glasgow)

Constraint programming (CP) is an expressive paradigm for modelling and solving problems stated in terms of finite-domain variables and arbitrary constraints. Many CP solvers are based on backtracking search, with interleaved propagation algorithms, which use sophisticated inference procedures to reduce the search space by filtering inconsistent values from the domains of variables.

This talk will be a tutorial on how we can modify a standard CP solver architecture to allow it to output a trustworthy and efficiently checkable certificate of correctness, both for satisfaction and optimisation problems. We'll see how pseudo-Boolean reasoning can be used to represent and derive facts about integer variables, linear inequalities, and even higher-level constraints such as "AllDifferent" (requiring a subset of variables to all take different values).

Proof logging for pseudo-Boolean optimization (Wietze Koops, Lund University and University of Copenhagen)

Certifying solvers have long been standard for Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead. While pseudo-Boolean proof logging has shown great potential to support proof logging for a wide range of combinatorial optimization paradigms, overheads have in most cases been far from what is required for real-world deployment. In this talk, I will show how to implement proof logging for pseudo-Boolean optimization, including techniques such as core-guided search and linear programming integration with Farkas certificates and cut generation, with a focus on how to ensure that proof logging and checking is efficient. Our experimental evaluation shows that proof logging and checking performance is now quite close to the level of SAT solving, and hence clearly practically feasible.

Proof logging for preprocessing/presolving in MaxSAT and 0-1 integer linear programming (Andy Oertel, Lund University and University of Copenhagen)

It is well-known that reformulating maximum satisfiability (MaxSAT) and mixed-integer programming (MIP) problems before solving is crucial for performance. While the overall goal of this reformulation process is the same in both communities, the concrete techniques used for preprocessing in MaxSAT and presolving in MIP are quite different. To ensure the correctness of different reformulations, all transformations must preserve the feasibility status and optimal value of the problem, but there is currently no established methodology to express and certify the equivalence between two optimization problems.

In this talk, it is presented how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MIP presolving and MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we obtain a formally verified end-to-end proof checking toolchain to verify the correctness of problem reformulations.

Proof logging for symmetry breaking (Markus Anders, RPTU Kaiserslautern-Landau)

Symmetry breaking is an indispensable technique when solving many interesting practical and mathematical problems. However, reasoning with symmetries is delicate and error-prone. Thus, correctness is an important concern. I will begin by giving a gentle introduction to symmetry breaking in SAT. Then I will show how these techniques can be proven correct using the so-called dominance rule. Lastly, I will briefly discuss recent progress and remaining challenges.

End-to-end verification for subgraph solving [demo] (Yong Kiam Tan, Institute for Infocomm Research, A*STAR, and Nanyang Technological University)

This is a demo-focused talk for the paper "End-to-End Verification for Subgraph Solving" (AAAI '24). I will give a brief tour of the CakePB codebase, showing how to build and formally verify an encoder frontend for certifying maximum clique size using pseudo-Booleam proofs. I will demonstrate the "end-to-end" part of CakePB verification---a correctness theorem that goes from the high-level mathematical semantics of cliques down to a machine-code correctness theorem about the executable proof checker.

A variety of trimming techniques for pseudo-Boolean proof logs (Arthur Gontier, University of Glasgow)

Trimming of proofs can be performed for multiple reasons. The most important purpose of trimming is to reduce proof checking time, but we can also think of situations where we want to be able to save as small a proof as possible as a certificate, or to use a proof to provide an explanation why a set of constraints is contradiction. We are developing tools for performing these tasks, and will present the main ideas behind the implementation as well as some early results.

Pseudo-Boolean proof logging for optimal classical planning (Simon Dold, University of Basel)

The solution to an optimal planning task is a sequence of actions with minimal cost that leads from the initial state to a goal state. Optimal planning is PSPACE-complete, and different approaches are used in practice to find an optimal solution. We introduce lower-bound certificates for classical planning tasks, which can be used to prove the optimality of a solution in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. We also demonstrate how to modify the A∗ algorithm to produce proofs of optimality.

Short, composable proofs without interference (Adrian Rebola-Pardo, TU Wien)

Interference is a phenomenon where inference rules in several practice-oriented proof systems (including the DRAT family and VeriPB) depend on the whole derived formula rather than specific derived clauses. While these rules generally allow more concise reasoning than interference-free proofs, interference prevents proofs from being easily composable. This creates many problems for trimming, proof logging in incremental solvers, and proof system design. This talk presents a novel approach to proof logging based on propositional dynamic logic, a multimodal logic that seems to suitable capture the semantics of interference-based reasoning without being itself affected by interference. I will also discuss how this can be leveraged to solve some limitations on existing proof systems.

Proof Logging in CaDiCaL (Florian Pollitt, Universität Freiburg)

This talks focuses on showcasing the state-of-the-art proof-logging support of the CaDiCaL SAT solver, covering a range of applications. Within this context, and from the perspective of a solver developer, I will discuss different needs and design decisions of proof formats and their impact on the development of CaDiCaL.

Symmetry breaking in the subgraph isomorphism problem (Ruth Hoffmann, University of St Andrews)

The subgraph isomorphism problem (SIP) asks, given a smaller (pattern) graph can we find it inside a larger (target) graph? The combinatorial search techniques used to answer this question follow the approaches used in SAT and CP, and thus should benefit from symmetry breaking.

We are introducing novel methods for symmetry breaking for SIP, both static and dynamic which can be applied to pattern graphs (variables) or target graphs (values). These techniques are rooted in group theory and are generic enough to be applicable to (almost) any combinatorial search problem.

The question that remains is, are we still solving the correct problem? I will talk through the correctness challenges we have encountered in the development of the technique, as well as the challenges that we are facing when going from a decision to an enumeration problem. This will hopefully lead to a discussion around how proof logging of symmetry breaking constraints might work.

Formal verification for constraint solvers (Catherine Dubois, ENSIIE)

This talk will outline my previous work on formalizing constraint solving with finite domains in a theorem prover. I will also share some thoughts on the alternative approach, proof logging, and proof verification.

Wishes for the VeriPB proof format: An update (Daniel Le Berre, Université d'Artois)

VeriPB proof logging has now been implemented fully in Sat4j, both for the resolution-based and the cutting-planes based solvers. The proofs produced during the PB25 competition have been verified successfully. This talk will discuss the lessons learned while integrating VeriPB proof logging in Sat4j.

Organizers

The WHOOPS '25 workshop was organized by Jakob Nordström at the University of Copenhagen and Lund University in collaboration with Ciaran McCreesh at the University of Glasgow.