Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Long Proofs of (Seemingly) Simple Formulas
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
2014 (English)In: THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2014, 2014, 121-137 p.Conference paper, Published paper (Refereed)
Abstract [en]

In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from so-called fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley 2011].

Place, publisher, year, edition, pages
2014. 121-137 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8561
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-158359DOI: 10.1007/978-3-319-09284-3_10ISI: 000345595300010Scopus ID: 2-s2.0-84958552506ISBN: 978-3-319-09284-3 (print)OAI: oai:DiVA.org:kth-158359DiVA: diva2:782272
Conference
17th International Conference on Theory and Applications of Satisfiability Testing (SAT) Held as Part of the Federated Logic Conference (FLoC) / Vienna Summer of Logic (VSL) Conference, JUL 09-24, 2014, Vienna, AUSTRIA
Note

QC 20150120

Available from: 2015-01-20 Created: 2015-01-07 Last updated: 2017-11-29Bibliographically approved
In thesis
1. On Complexity Measures in Polynomial Calculus
Open this publication in new window or tab >>On Complexity Measures in Polynomial Calculus
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Proof complexity is the study of different resources that a proof needs in different proof systems for propositional logic. This line of inquiry relates to the fundamental questions in theoretical computer science, as lower bounds on proof size for an arbitrary proof system would separate P from NP.

We study two simple proof systems: resolution and polynomial calculus. In resolution we reason using clauses, while in polynomial calculus we use polynomials. We study three measures of complexity of proofs: size, space, and width/degree. Size is the number of clauses or monomials that appear in a resolution or polynomial calculus proof, respectively. Space is the maximum number of clauses/monomials we need to keep at each time step of the proof. Width/degree is the size of the largest clause/monomial in a proof.

Width is a lower bound for space in resolution. The original proof of this claim used finite model theory. In this thesis we give a different, more direct proof of the space-width relation. We can ask whether a similar relation holds between space and degree in polynomial calculus. We make some progress on this front by showing that when a formula F requires resolution width w then the XORified version of F requires polynomial calculus space Ω(w). We also show that space lower bounds do not imply degree lower bounds in polynomial calculus.

Width/degree and size are also related, as strong lower bounds for width/degree imply strong lower bounds for size. Currently, proving width lower bounds has a well-developed machinery behind it. However, the degree measure is much less well-understood. We provide a unified framework for almost all previous degree lower bounds. We also prove some new degree and size lower bounds. In addition, we explore the relation between theory and practice by running experiments on some current state-of-the-art SAT solvers.

Place, publisher, year, edition, pages
Stockholm, Sweden: KTH Royal Institute of Technology, 2016. 180 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:02
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-197278 (URN)978-91-7729-226-5 (ISBN)
Public defence
2017-01-20, D2, Lindstedtsvägen 5, Stockholm, 14:00 (English)
Opponent
Supervisors
Projects
Understanding the Hardness of Theorem Proving
Funder
EU, FP7, Seventh Framework Programme, 279611
Note

QC 20161206

Available from: 2016-12-06 Created: 2016-11-30 Last updated: 2016-12-26Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Nordström, Jakob

Search in DiVA

By author/editor
Miksa, MladenNordström, Jakob
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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