Open Collections

Proof Systems for Pseudo-Boolean Solving

Banff International Research Station for Mathematical Innovation and Discovery

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.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: Tata Institute of Fundamental Research

2019-03-31

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/69368

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/