BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Proof Systems for Pseudo-Boolean Solving Vinyals, Marc


Pseudo-Boolean solvers that generalize the CDCL algorithm and reason within the cutting planes proof system can have a theoretical advantage with respect to solvers that just translate the problem and apply the standard CDCL algorithm, which is limited to resolution. In practice, however, results are mixed. Do we need a better theory, better solvers, or both

One key observation is that implementation constraints limit solvers to a subset of inference rules. In this talk we identify subsystems of cutting planes that arise from these limited rules and we classify them, showing in particular that pseudo-Boolean solvers are limited to resolution if their input is encoded adversarially.

Guided by these theoretical insights we craft formulas that lie within the limits of pseudo-Boolean solvers and test them in practice. Alas, current solvers perform terribly on these benchmarks, but we can at least extract concrete obstacles for upcoming solvers to overcome.

Joint work with Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and Jakob Nordström.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International