We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

A Proof Complexity View of Pseudo-Boolean Solving

Formal Metadata

Title
A Proof Complexity View of Pseudo-Boolean Solving
Alternative Title
Proof Systems for Pseudo-Boolean Solving
Title of Series
Number of Parts
28
Author
Contributors
License
CC Attribution - NonCommercial - NoDerivatives 4.0 International:
You are free to use, copy, distribute and transmit the work or content in unchanged form for any legal and non-commercial purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
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.