Standard
Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers. / Elffers, Jan; Giráldez-Cru, Jesús; Nordström, Jakob; Vinyals, Marc.
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. 75-93 (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
Elffers, J, Giráldez-Cru, J
, Nordström, J & Vinyals, M 2018,
Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers. 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. 75-93, 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_5APA
Elffers, J., Giráldez-Cru, J.
, Nordström, J., & Vinyals, M. (2018).
Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers. 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. 75-93). 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_5Vancouver
Elffers J, Giráldez-Cru J
, Nordström J, Vinyals M.
Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers. 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. 75-93. (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_5Author
Elffers, Jan ; Giráldez-Cru, Jesús ; Nordström, Jakob ; Vinyals, Marc. / Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers. 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. 75-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 10929 LNCS).
Bibtex
@inproceedings{d78db1544a844bb68df76b02b6615b86,
title = "Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers",
abstract = "We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also real-valued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.",
author = "Jan Elffers and Jes{\'u}s Gir{\'a}ldez-Cru and Jakob Nordstr{\"o}m and Marc Vinyals",
year = "2018",
doi = "10.1007/978-3-319-94144-8_5",
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 = "75--93",
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 - Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers
AU - Elffers, Jan
AU - Giráldez-Cru, Jesús
AU - Nordström, Jakob
AU - Vinyals, Marc
PY - 2018
Y1 - 2018
N2 - We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also real-valued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.
AB - We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also real-valued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.
UR - http://www.scopus.com/inward/record.url?scp=85049662965&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-94144-8_5
DO - 10.1007/978-3-319-94144-8_5
M3 - Article in proceedings
AN - SCOPUS:85049662965
SN - 9783319941431
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 75
EP - 93
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,
T2 - 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018
Y2 - 9 July 2018 through 12 July 2018
ER -
