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
In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving
Inst Fundamental Res, Mumbai, Maharashtra, India.
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.
Show others and affiliations
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. 292-310Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2018. Vol. 10929, p. 292-310
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
Identifiers
URN: urn:nbn:se:kth:diva-238362DOI: 10.1007/978-3-319-94144-8_18ISI: 000490902900018Scopus ID: 2-s2.0-85049666666ISBN: 9783319941431 (print)OAI: oai:DiVA.org:kth-238362DiVA, id: diva2:1262530
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

OC 20181812. QC 20191106

Available from: 2018-11-12 Created: 2018-11-12 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, JakobGocht, StephanNordström, Jakob

Search in DiVA

By author/editor
Elffers, JanGiráldez-Cru, JakobGocht, StephanNordström, Jakob
By organisation
Theoretical Computer Science, TCS
Other Engineering and Technologies

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 47 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