Abstract
Since about two decades, the strength of the cutting planes proof system has motivated the development of pseudo-Boolean (PB) solvers based on the CDCL architecture at the core of the efficiency of modern SAT solvers. In theory, such solvers should be able to produce exponentially shorter proofs, but in practice, resolution based SAT solvers remain more efficient on many benchmarks. This is partly due to the fact that implementing the CDCL architecture in a PB context is not as straightforward as it may appear at first sight. More precisely, many invariants of the CDCL algorithm are not preserved when dealing with PB constraints.
In this talk, we will introduce different techniques that have been designed to deal with such broken invariants (especially to detect propagations and to preserve conflicts) and discuss their limitations and the problems they raise. We will also present some open questions that are specific to PB solvers and may have an impact on the strength of their reasoning.