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

Formale Metadaten

Titel
A Proof Complexity View of Pseudo-Boolean Solving
Alternativer Titel
Proof Systems for Pseudo-Boolean Solving
Serientitel
Anzahl der Teile
28
Autor
Mitwirkende
Lizenz
CC-Namensnennung - keine kommerzielle Nutzung - keine Bearbeitung 4.0 International:
Sie dürfen das Werk bzw. den Inhalt in unveränderter Form zu jedem legalen und nicht-kommerziellen Zweck nutzen, vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
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.