Standard
In between resolution and cutting planes : A study of proof systems for pseudo-boolean SAT solving. / Vinyals, Marc; Elffers, Jan; Giráldez-Cru, Jesús; Gocht, Stephan; Nordström, Jakob.
Theory and Applications of Satisfiability Testing – SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Olaf Beyersdorff; Christoph M. Wintersteiger. Springer Verlag, 2018. p. 292-310 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 10929 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
Vinyals, M, Elffers, J, Giráldez-Cru, J, Gocht, S
& Nordström, J 2018,
In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving. in O Beyersdorff & CM Wintersteiger (eds),
Theory and Applications of Satisfiability Testing – SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10929 LNCS, pp. 292-310, 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom,
09/07/2018.
https://doi.org/10.1007/978-3-319-94144-8_18APA
Vinyals, M., Elffers, J., Giráldez-Cru, J., Gocht, S.
, & Nordström, J. (2018).
In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving. In O. Beyersdorff, & C. M. Wintersteiger (Eds.),
Theory and Applications of Satisfiability Testing – SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 292-310). Springer Verlag,. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 10929 LNCS
https://doi.org/10.1007/978-3-319-94144-8_18Vancouver
Vinyals M, Elffers J, Giráldez-Cru J, Gocht S
, Nordström J.
In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving. In Beyersdorff O, Wintersteiger CM, editors, Theory and Applications of Satisfiability Testing – SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag,. 2018. p. 292-310. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 10929 LNCS).
https://doi.org/10.1007/978-3-319-94144-8_18Author
Vinyals, Marc ; Elffers, Jan ; Giráldez-Cru, Jesús ; Gocht, Stephan ; Nordström, Jakob. / In between resolution and cutting planes : A study of proof systems for pseudo-boolean SAT solving. 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 / Olaf Beyersdorff ; Christoph M. Wintersteiger. Springer Verlag, 2018. pp. 292-310 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 10929 LNCS).
Bibtex
@inproceedings{f7a877063a0e4883a6cd468b4aea87cd,
title = "In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving",
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 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.",
author = "Marc Vinyals and Jan Elffers and Jes{\'u}s Gir{\'a}ldez-Cru and Stephan Gocht and Jakob Nordstr{\"o}m",
year = "2018",
doi = "10.1007/978-3-319-94144-8_18",
language = "English",
isbn = "9783319941431",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag,",
pages = "292--310",
editor = "Olaf Beyersdorff and Wintersteiger, {Christoph M.}",
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",
note = "21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",
}
RIS
TY - GEN
T1 - In between resolution and cutting planes
T2 - 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018
AU - Vinyals, Marc
AU - Elffers, Jan
AU - Giráldez-Cru, Jesús
AU - Gocht, Stephan
AU - Nordström, Jakob
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85049666666&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-94144-8_18
DO - 10.1007/978-3-319-94144-8_18
M3 - Article in proceedings
AN - SCOPUS:85049666666
SN - 9783319941431
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 292
EP - 310
BT - Theory and Applications of Satisfiability Testing – SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
A2 - Beyersdorff, Olaf
A2 - Wintersteiger, Christoph M.
PB - Springer Verlag,
Y2 - 9 July 2018 through 12 July 2018
ER -
