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 Citations and Data
Attribution-NonCommercial-NoDerivatives 4.0 International