Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-8963-6299
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
Tata Institute of Fundamental Research, Mumbai, India.
2018 (English)In: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Springer, 2018, Vol. 10929, p. 75-93Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2018. Vol. 10929, p. 75-93
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10929
National Category
Other Engineering and Technologies not elsewhere specified
Identifiers
URN: urn:nbn:se:kth:diva-238355DOI: 10.1007/978-3-319-94144-8_5ISI: 000490902900005Scopus ID: 2-s2.0-85049662965ISBN: 9783319941431 (print)OAI: oai:DiVA.org:kth-238355DiVA, id: diva2:1261741
Conference
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, 9-12 July 2018
Note

QC 20181108. QC 20191106

Available from: 2018-11-08 Created: 2018-11-08 Last updated: 2019-11-06Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Elffers, JanGiráldez-Cru, JakobNordström, Jakob

Search in DiVA

By author/editor
Elffers, JanGiráldez-Cru, JakobNordström, Jakob
By organisation
Theoretical Computer Science, TCS
Other Engineering and Technologies not elsewhere specified

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 152 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf