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
Space proof complexity for random 3-CNFs
KTH, School of Computer Science and Communication (CSC).
Show others and affiliations
2017 (English)In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 255, p. 165-176Article in journal (Refereed) Published
Abstract [en]

We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF phi in n variables requires, with high probability, Omega(n) distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of phi requires, with high probability, Omega(n) clauses each of width Omega(n) to be kept at the same time in memory. This gives a Omega(n(2)) lower bound for the total space needed in Resolution to refute phi. These results are best possible (up to a constant factor) and answer questions about space complexity of 3-CNFs. The main technical innovation is a variant of Hall's Lemma. We show that in bipartite graphs with bipartition (L, R) and left-degree at most 3, L can be covered by certain families of disjoint paths, called VW-matchings, provided that L expands in R by a factor of (2 - is an element of), for is an element of< 1/5.

Place, publisher, year, edition, pages
Elsevier, 2017. Vol. 255, p. 165-176
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-214517DOI: 10.1016/j.ic.2017.06.003ISI: 000407658600008Scopus ID: 2-s2.0-85021162863OAI: oai:DiVA.org:kth-214517DiVA, id: diva2:1145773
Note

QC 20170929

Available from: 2017-09-29 Created: 2017-09-29 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Bonacina, Ilario

Search in DiVA

By author/editor
Bonacina, Ilario
By organisation
School of Computer Science and Communication (CSC)
In the same journal
Information and Computation
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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