Jakob Nordström / SLOPPY '24

1st International Workshop on Solving Linear Optimization Problems for Pseudo-Booleans and Yonder (SLOPPY '24)

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

Background

The Boolean satisfiability (SAT) problem is one of the most fascinating problems in computer science and mathematics. Though it is deceptively easy to state—given a formula in propositional logic, is it possible to assign variables true and false so that the formula evaluates to true?—it has been the focus of extensive research ever since the dawn of computer science. SAT was the first problem to be proven NP-complete in the early 1970s, and a widely accepted hypothesis is that it requires exponential time to solve in the worst case. Yet since the turn of the millennium there have been dramatic performance improvements of SAT solvers based on conflict-driven clause learning (CDCL), and today CDCL solvers are routinely used to solve large-scale real-world problems in, e.g., hardware and software verification, AI planning, automated theorem proving, and many other areas. This success has also led to exports of the conflict-driven paradigm beyond SAT solving to different types of optimization problems.

A drawback with CDCL is that from a mathematical point of view the method of reasoning is quite weak—it is based on the resolution proof system, for which exponential lower bounds are known even for simple combinatorial principles. Another issue is that the problems to be solved have to be encoded in conjunctive normal form (CNF) as a collection of disjunctive clauses, which leads to a loss in information compared to higher-level constraints and negatively affects the reasoning power.

An attractive option is to instead use (linear) pseudo-Boolean (PB) constraints, i.e., 0-1 integer linear inequalities. Such constraints provide a succinct way of encoding a wide variety of computational tasks, including problems with an objective function to be optimized. Pseudo-Boolean constraints are more expressive than CNF, but are close enough that CNF-based techniques can be harnessed to attack pseudo-Boolean problems. The connection to integer linear programming (ILP) makes it natural to also borrow insights from this area. Some pseudo-Boolean solvers are still based on resolution, in that an important part of the solving process is to translate the input to CNF and use the CDCL algorithm. Another approach, however, is to go beyond resolution and build solvers using the cutting planes proof system, which is known to be exponentially stronger than resolution in theory. Although harnessing this increased power algorithmically is a far from trivial task, there have been notable successes with solvers such as Sat4j developed by Daniel Le Berre's group at Université d'Artois and RoundingSat from the Mathematical Insights into Algorithms for Optimization (MIAO) group in Copenhagen/Lund, as well as other tools developed on top of these solvers.

Purpose of This Workshop

To highlight and celebrate these developments, we are organizing an informal workshop for people working on pseudo-Boolean solving and optimization and related problems. The idea is to meet for a few days to hear technical presentations of recent and ongoing research and also discuss the potential for collaboration on research and/or solver development in different directions. The workshop will focus on pseudo-Boolean solvers and techniques that operate natively on 0-1 integer linear inequalities, rather than with CNF encodings of such inequalities. However, pseudo-Boolean techniques have recently come up also in contexts such as mixed integer linear programming (MIP) and constraint programming (CP), and CNF encodings can also be of interest even for native pseudo-Boolean solvers, so the focus described above is intended to be inclusive rather than exclusive.

Possible interesting topics for discussion could include, but would not be limited to:

pseudo-Boolean conflict analysis and propagation,
optimization techniques on top of pseudo-Boolean decision oracles (inspired by MaxSAT and other areas),
proof logging techniques to make pseudo-Boolean solvers certifying,
integration of techniques from MIP and CP,
exports of techniques to MIP and CP.

Clearly, the most important aspect of any endeavour like this is to choose a suitable name for the event. It has been proposed that a title like Workshop on Solving Linear Optimization Problems for Pseudo-Booleans and Yonder, which obviously abbreviates to SLOPPY, would convey well the goal of carefully designing highly efficient but logically sound combinatorial solvers that can ideally use proof logging to generate provably correct results.

Workshop Program

The workshop will be held over three days, with a tutorial day on Tuesday November 5 followed by two days of technical talks and discussions on Wednesday November 6 and Thursday November 7. Workshop participants are warmly welcome to visit for the full week if so desired.

The workshop will be held at the Department of Computer Science at Lund University, but the presentations will also be streamed over Zoom.

TUESDAY NOVEMBER 5 (TUTORIAL DAY) IN E:1426
09:00-10:30	Tutorial on Boolean Satisfiability (SAT) Solving	Jakob Nordström
10:30-11:00	Morning break
11:00-12:30	Tutorial on Conflict-Driven Pseudo-Boolean Solving	Jakob Nordström
12:30-14:00	Lunch
14:00-15:30	Tutorial on Conflict-Driven Pseudo-Boolean Optimization	Jakob Nordström
15:30-16:00	Afternoon break
16:00-17:30	Tutorial on Mixed Integer Linear Programming (MIP) and Pseudo-Boolean Optimization	Jakob Nordström
19:45	Workshop dinner at Mat & Destillat at Kyrkogatan 17 in downtown Lund

WEDNESDAY NOVEMBER 6 IN E:1147
09:00-10:00	A MIP Perspective on Pseudo-Boolean Optimization	Alexander Tesch
10:00-10:30	Morning break with presentation of participants
10:30-11:30	Oracle-Based Local Search for Pseudo-Boolean Optimization	Jeremias Berg
11:30-12:30	Branch-and-Bound MaxSAT Solving with MaxCDCL	Jordi Coll
12:30-14:00	Lunch
14:00-15:00	A Conflict-Free Learning Approach for MILP and WCSP Optimisation	Pierre Montalbano
15:00-18:00	Time for discussions in rooms E:1147 and E:2113C ("Small CS meeting room")

THURSDAY NOVEMBER 7 IN E:1426
09:00-10:00	Faster Unit Propagation in Pseudo-Boolean Solving	Rui Zhao
10:00-11:00	Proof Logging for Branch-and-Bound MaxSAT with MaxCDCL	Dieter Vandesande
11:00-11:30	Morning break
11:30-12:00	Pseudo-Boolean Proof Logging for RoundingSat	Marc Vinyals
12:00-12:30	Wishes for the VeriPB proof format	Daniel Le Berre [over Zoom]
12:30-14:00	Lunch and end of workshop presentations
14:00-18:00	Time for discussions in rooms E:1426 and E:2113C ("Small CS meeting room")

Titles and Abstracts of Contributed Presentations

Alexander Tesch (BoolAI): A MIP Perspective on Pseudo-Boolean Optimization

In this talk, we address pseudo-Boolean optimization through the lense of Mixed-Integer Programming (MIP). In particular, we will present an alternative approach to PB conflict analysis which performs sequential lifting of the underlying knapsack polytopes of the reason and conflict constraints. We will give a first theoretical and practical comparison between our approach and a few more common approaches from the PB literature such as MIR cuts and (partial-) weakening. In the end, we also give an outlook on more advanced cut-generation techniques from the MIP literature that could be applied to PB conflict analysis and core-guided search.

Jeremias Berg (University of Helsinki): Oracle-Based Local Search for Pseudo-Boolean Optimization

Oracle-based local search is a recently proposed approach to anytime constraint optimization that aims to find good, though not provably, optimal solutions quickly. The approach can be seen as a type of stochastic local search in which a decision oracle for the underlying constraint language is used to move from solution to solution. Using highly effective CDCL SAT solvers as oracles, oracle-based local search has been highly successful in anytime maximum satisfiability (MaxSAT). Solvers implementing the approach regularly top the results of recent MaxSAT evaluations.

In this talk, I will outline our recent (published at ECAI 23) work in extending oracle-based Local Search to the more general paradigm of pseudo-Boolean optimization (PBO). As a basis for the approach, we use recent advances in practical approaches to checking the satisfiability of pseudo-Boolean constraints. We outline various heuristics within the oracle-based approach to anytime PBO solving and show that the approach compares in practice favorably and orthogonally, both to a recently proposed local search approach for PBO that is in comparison to a more traditional instantiation of the stochastic local search paradigm and a recent exact PBO approach used as an anytime solver.

Jordi Coll (Universitat de Girona): Branch-and-Bound MaxSAT Solving with MaxCDCL

MaxSAT is a widely studied NP-hard optimization problem due to its broad utility in modeling and solving diverse optimization problems of practical interest. Branch-and-Bound (BnB) MaxSAT solvers had shown to be an efficient approach to solving random and crafted instances, but had traditionally failed to be as competitive as SAT-based MaxSAT solvers when dealing with instances of industrial nature. However, this has changed recently with the introduction of the MaxCDCL algorithm, which effectively integrates clause learning into BnB to solve MaxSAT. In this talk we provide a detailed description of the MaxCDCL algorithm, deepen in relevant implementation details and show how this approach relates to and differs from other approaches to MaxSAT. We will place special emphasis on the lookahead procedure to compute a lower bound of the cost of a partial assignment—which is the core and distinguishing part of MaxCDCL—and its integration with a CDCL-based solver.

Pierre Montalbano (Université de Tours): A Conflict-Free Learning Approach for MILP and WCSP Optimisation

Weighted Constraint Satisfaction Problems (WCSP) are an extension of the classic Constraint Satisfaction Problem (CSP), where costs (or weights) are associated with constraint violations. The objective is to find an assignment that minimizes the total constraint violation. Solving WCSPs typically relies on backtracking search and constraint propagation to compute lower bounds. It has the ability to handle global constraints, but it often requires a dedicated algorithm to propagate them.

Guided by the success of conflict-based learning methods in multiple domains (such as SAT, Pseudo-Boolean Optimization, or ILP), we designed a new conflict-free learning mechanism. This mechanism aims to memorize, through a linear constraint, the lower bounds of encountered sub-problems. If the same sub-problem (or a similar one) reappears in the search, propagating the previously learned constraint will help to obtain a stronger lower bound. This learning mechanism is conflict-free, meaning that it doesn't require a conflict to be triggered and can be used to learn a constraint at every node of a search tree.

Our approach integrates techniques from CP, ILP, and PBO, and we show how it can be embedded inside a classic MILP solver before extending it to WCSP solvers. We implemented this learning mechanism in a simple solver performing branch-and-bound and using CPLEX to solve the LP at every node. We show that it can significantly decrease the number of visited nodes for the knapsack problem or kb-tree (instances with a bounded treewidth).

Rui Zhao (Universitat Politècnica de Catalunya): Faster Unit Propagation in Pseudo-Boolean Solving

Unit propagation is known to be one of the most time-consuming procedures inside CDCL-based SAT solvers. Not surprisingly, it has been studied in depth and the two-watched-literal scheme, enhanced with implementation details boosting its performance, has emerged as the dominant method. In pseudo-Boolean solvers, the importance of unit propagation is similar, but no dominant method exists: counter propagation and watched-based extensions are efficient for different types of constraints, which has opened the door to hybrid methods. However, probably due to the higher complexity of implementing pseudo-Boolean solvers, research efforts have not focused much on concrete implementation details for unit propagation but rather on higher-level aspects of other procedures, such as conflict analysis. In this talk, we will present (i) a novel methodology to precisely assess the performance of propagation mechanisms, (ii) an evaluation of implementation variants of the propagation methods present in RoundingSat and (iii) a detailed analysis showing that hybrid methods outperform the ones based on a single technique. Our final conclusion will be that a carefully implemented hybrid propagation method is considerably faster than the preferred propagation mechanism in RoundingSat, and that this improvement leads to a better overall performance of the solver.

Dieter Vandesande (Vrije Universiteit Brussel): Proof Logging for Branch-and-Bound MaxSAT with MaxCDCL

In earlier work, MaxSAT solvers implementing both solution-improving as well as 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, we will cover the solver MaxCDCL, which combines Branch-and-Bound search with the power of clause learning as it is implemented in SAT solvers.

Marc Vinyals (University of Auckland): Proof Logging for RoundingSat

We discuss how proof logging is implemented in RoundingSAT. While pseudo-Boolean conflict analysis can be logged using standard cutting planes rules, and this still applies to linear search optimisation, logging core-guided optimisation requires a more careful implementation. In particular, we discuss how to log lazy reified variables, objective reformulation, and hardening.

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

Two proofs logging have been added to Sat4j in 2024: IDRUP and VeriPB 2.0. The two proof formats had the common feature to encompass several calls to the SAT solver, contrariwise to UNSAT proofs certificates in DRUP or VeriPB 1.0: it required some small changes in Sat4j. When Sat4j was submitted to the PB evaluation, it happened that many simplifications and normalisations performed in Sat4j required a VeriPB justifications when using the cutting planes proof system but not the resolution based one. This prevented Sat4j CP to participate to the certified tracks. The presentation will present some lessons learned when adding those proof formats in Sat4j and will focus on potential improvements in VeriPB to simplify its adoption by solvers designers.

Practicalities

Workshop Location

The workshop will be held at the Department of Computer Science at Lund University at Klas Anshelms väg 10 / Ole Römers väg 3.

Food and Accommodation

Workshop lunches are at your own expense, but an option favoured by the MIAO group is Bryggan, which is just a few minutes away by foot from the CS department.

Lund University has a guest house for visitors, which is not superfancy but might be cheaper than hotel options. If you are interested in inquiring whether it is possible to book a room at the guest house, then please send a message to Jakob Nordström well ahead of time to get connected to Lund University administration.

There should also be a generous selection of hotels in Lund available at your favourite travel booking site. Lund is a half-hour train ride away from Copenhagen Airport and one hour away from central Copenhagen, where hotels are likely to be markedly more expensive than on the Swedish side of the Öresund Bridge.

Directions to Lund

If you are travelling by air, the Copenhagen Airport Kastrup (CPH) is probably the most convenient option, although Malmö Airport (MMX) in Sturup might also be an alternative. From Copenhagen Airport you take the train to Lund. From Malmö Airport there are airport buses to Malmö, and then you take a 10-minute train ride onwards to Lund. Below follow directions to Lund from Copenhagen.

To get to the CS department at Lund University from Copenhagen Airport, take the Öresund commuter train across the Öresund Bridge to Lund. Please do not forget to bring your passport along, as you will be crossing the border between Sweden and Denmark and there are sometimes passport controls. All commuter trains from Copenhagen to any destination in Sweden will pass through Lund ca 10 minutes after Malmö Central Station.

The easiest way of buying tickets to Sweden might be to download the Skånetrafiken app. You can adjust the settings so that you get e-mailed receipts for all purchases. There are also ticket machines at Copenhagen Airport.

The most convenient route onwards from Lund Central Station would seem to be to take the tram to the "Lund LTH" stop, which takes just a few minutes, and then walk from there a few minutes minutes more. If you are coming with the standard Öresund commuter train from Copenhagen, then the local public transport in Lund is included in your train ticket.

To reach the tram stop, take the stairs at the middle exit of the platform at Lund Central Station (usually at the front of the train in the direction of travel if you are coming from Copenhagen/Malmö, or close to the first train cars), take a right, and then walk straight out of the train station and cross one small and one slightly larger street. Now you should see a bus stop to your left, and some 20-30 meters behind that bus stop there is a tram station.

After getting off the tram at the "Lund LTH" stop, walk right to John Ericssons väg and continue straight, then take a right before you reach the Vattenhallen Science Center to reach the main entrance at Klas Anshelms väg 10. To get to the MIAO research group, bear right after you have entered the building and walk up the stairs one floor up, take a left turn and then immediately a right turn — you should now be in front of a locked door with a sign "Datavetenskap" (i.e., Computer Science). If anyone is there and opens for you, then just continue straight past a few doors until you see offices with the MIAO logo. Otherwise, try to text or call Jakob Nordström or some other MIAO group member.

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.