2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25)Executive SummaryThe 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25) will be 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 is in turn part of the Final EuroProofNet Symposium. Background and PurposeSince 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 will be 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 is 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 FundingRegistration is free but mandatory. Due to strong interest, the EuroProofNet Symposium organizers have now had to close registration, and we cannot accept additional participants. VenueWHOOPS '25 will be held at Institut Pascal at 530 Rue André Rivière, 91400 Orsay (see map). We will also provide the option of attending the workshop online (barring unexpected technical hiccups), but the necessary information to attends online needs to be requested from the organizers. Please follow the links for information about local travel directions, nearby hotels, and food options. Note that lunch and dinner is not provided, but have to be organised on your own, and the number of options during the weekend is somewhat limited. In particular, dining selections on Sunday September 14 are very limited and so some advance planning is highly recommended. One piece of advice from the symposium organizers is to buy some food for lunch at the Supermarket Intermarché Express on Sunday morning. Two other options that seem to be open on Sunday are Bap Meokja and O'9 Poke. On Sunday, the institute building will be locked for security reasons, but a number of access cards will be distributed among WHOOPS '25 participants. To be on the safe side, it might be a good idea to write down the cell phone number of the WHOOPS '25 main organizer Jakob Nordström, so that you can call if you would accidentally get locked out. Workshop ProgramThe workshop program is structured as follows:
Please contact Jakob Nordström if you would be interested in giving a presentation at the WHOOPS '25 workshop (virtually or on site).
Titles and Abstracts of PresentationsAn 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. OrganizersThe WHOOPS '25 workshop is organized by Jakob Nordström at the University of Copenhagen and Lund University in collaboration with Ciaran McCreesh at the University of Glasgow. |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||