Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers
(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.75-93- 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... (More)
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.
(Less)
- author
- Elffers, Jan LU ; Giráldez-Cru, Jesús ; Nordström, Jakob LU and Vinyals, Marc
- 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:85049662965
- ISSN
- 1611-3349
- 0302-9743
- ISBN
- 9783319941431
- DOI
- 10.1007/978-3-319-94144-8_5
- language
- English
- LU publication?
- no
- id
- 71a93924-e33a-43ad-bca2-7da1e022541d
- date added to LUP
- 2020-12-18 22:19:01
- date last changed
- 2024-01-17 19:02:16
@inproceedings{71a93924-e33a-43ad-bca2-7da1e022541d,
abstract = {{<p>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.</p>}},
author = {{Elffers, Jan and Giráldez-Cru, Jesús and Nordström, Jakob and Vinyals, Marc}},
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 = {{1611-3349}},
language = {{eng}},
pages = {{75--93}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers}},
url = {{http://dx.doi.org/10.1007/978-3-319-94144-8_5}},
doi = {{10.1007/978-3-319-94144-8_5}},
volume = {{10929}},
year = {{2018}},
}