BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Towards Faster Conflict-Driven Pseudo-Boolean Solving Nordstrom, Jakob


The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability---so-called SAT solvers---and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning (a.k.a. 0-1 integer linear programming), but so far the promise of exponential gains in performance has mostly failed to materialize---the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior.

In this talk, we will discuss conflict-driven search and how to lift it from clauses to pseudo-Boolean linear constraints. We will survey the "classic" method in [Chai and Kuehlmann '05] based on saturation, and then describe a relatively new approach from [Elffers and Nordström '18] instead using division. We will also try to highlight some of the obstacles that remain along the path to truly efficient pseudo-Boolean solvers.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International