In between resolution and cutting planes : A study of proof systems for pseudo-boolean SAT solving
(2018) 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018 In Lecture Notes in Computer Science 10929. p.292-310- Abstract
We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but... (More)
We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP—which would require major technical breakthroughs in proof complexity—these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers.
(Less)
- author
- Vinyals, Marc ; Elffers, Jan LU ; Giráldez-Cru, Jesús ; Gocht, Stephan LU and Nordström, Jakob LU
- publishing date
- 2018
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Theory and Applications of Satisfiability Testing – SAT 2018 : 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
- series title
- Lecture Notes in Computer Science
- editor
- Beyersdorff, Olaf and Wintersteiger, Christoph M.
- volume
- 10929
- pages
- 19 pages
- publisher
- Springer
- conference name
- 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018
- conference location
- Oxford, United Kingdom
- conference dates
- 2018-07-09 - 2018-07-12
- external identifiers
-
- scopus:85049666666
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783319941431
- DOI
- 10.1007/978-3-319-94144-8_18
- language
- English
- LU publication?
- no
- id
- 3a0e054f-c05a-4dd8-b3c7-1b7f4b917a23
- date added to LUP
- 2020-12-18 22:18:41
- date last changed
- 2024-05-01 23:47:04
@inproceedings{3a0e054f-c05a-4dd8-b3c7-1b7f4b917a23,
abstract = {{<p>We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP—which would require major technical breakthroughs in proof complexity—these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers.</p>}},
author = {{Vinyals, Marc and Elffers, Jan and Giráldez-Cru, Jesús and Gocht, Stephan and Nordström, Jakob}},
booktitle = {{Theory and Applications of Satisfiability Testing – SAT 2018 : 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings}},
editor = {{Beyersdorff, Olaf and Wintersteiger, Christoph M.}},
isbn = {{9783319941431}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{292--310}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{In between resolution and cutting planes : A study of proof systems for pseudo-boolean SAT solving}},
url = {{http://dx.doi.org/10.1007/978-3-319-94144-8_18}},
doi = {{10.1007/978-3-319-94144-8_18}},
volume = {{10929}},
year = {{2018}},
}