1st International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '24)BackgroundSince 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. ProgramDuring 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.
About the MIAO Research GroupThe 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. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||