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
Clique Is Hard on Average for Regular Resolution
Univ Politecn Cataluna, Dept Comp Sci, Barcelona, Spain..
Univ Politecn Cataluna, Dept Comp Sci, Barcelona, Spain..
KTH, School of Electrical Engineering and Computer Science (EECS).
Sapienza Univ Roma, Dept Stat Sci, Rome, Italy..
Show others and affiliations
2018 (English)In: STOC'18: PROCEEDINGS OF THE 50TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING / [ed] Diakonikolas, I Kempe, D Henzinger, M, ASSOC COMPUTING MACHINERY , 2018, p. 866-877Conference paper, Published paper (Refereed)
Abstract [en]

We prove that for k << (4)root n regular resolution requires length n(Omega(k)) to establish that an Erdos Renyi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional n(Omega(k)) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.

Place, publisher, year, edition, pages
ASSOC COMPUTING MACHINERY , 2018. p. 866-877
Keywords [en]
Proof complexity, regular resolution, k-clique, Erdos-Renyi random graphs
National Category
Discrete Mathematics
Identifiers
URN: urn:nbn:se:kth:diva-244573DOI: 10.1145/3188745.3188856ISI: 000458175600074Scopus ID: 2-s2.0-85043471352OAI: oai:DiVA.org:kth-244573DiVA, id: diva2:1294866
Conference
50th Annual ACM Symposium on Theory of Computing, STOC 2018; Los Angeles; United States; 25 June 2018 through 29 June 2018
Note

QC 20190308

Available from: 2019-03-08 Created: 2019-03-08 Last updated: 2019-07-29Bibliographically approved
In thesis
1. Lower Bounds and Trade-offs in Proof Complexity
Open this publication in new window or tab >>Lower Bounds and Trade-offs in Proof Complexity
2019 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Propositional proof complexity is a field in theoretical computer science that analyses the resources needed to prove statements. In this thesis, we are concerned about the length of proofs and trade-offs between different resources, such as length and space.

A classical NP-hard problem in computational complexity is that of determining whether a graph has a clique of size k. We show that for all k ≪ n^(1/4) regular resolution requires length n^Ω(k) to establish that an Erdős–Rényi graph with n vertices and appropriately chosen edge density does not contain a k-clique. In particular, this implies an unconditional lower bound on the running time of state-of-the-artalgorithms for finding a maximum clique.

In terms of trading resources, we prove a length-space trade-off for the cutting planes proof system by first establishing a communication-round trade-off for real communication via a round-aware simulation theorem. The technical contri-bution of this result allows us to obtain a separation between monotone-AC^(i-1) and monotone-NC^i.

We also obtain a trade-off separation between cutting planes (CP) with unbounded coefficients and cutting planes where coefficients are at most polynomial in thenumber of variables (CP*). We show that there are formulas that have CP proofs in constant space and quadratic length, but any CP* proof requires either polynomial space or exponential length. This is the first example in the literature showing any type of separation between CP and CP*.

For the Nullstellensatz proof system, we prove a size-degree trade-off via a tight reduction of Nullstellensatz refutations of pebbling formulas to the reversible pebbling game. We show that for any directed acyclic graph G it holds that G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatzrefutation of the pebbling formula over G in size t + 1 and degree s.

Finally, we introduce the study of cumulative space in proof complexity, a measure that captures the space used throughout the whole proof and not only the peak space usage. We prove cumulative space lower bounds for the resolution proof system, which can be viewed as time-space trade-offs where, when time is bounded, space must be large a significant fraction of the time.

Place, publisher, year, edition, pages
KTH Royal Institute of Technology, 2019. p. 247
Series
TRITA-EECS-AVL ; 2019:47
Keywords
Proof complexity, trade-offs, lower bounds, size, length, space
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-249610 (URN)978-91-7873-191-6 (ISBN)
Public defence
2019-06-14, Kollegiesalen, Brinellvägen 8, Stockholm, 14:00 (English)
Opponent
Supervisors
Note

QC 20190527

Available from: 2019-05-27 Created: 2019-05-24 Last updated: 2019-05-27Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

de Rezende, Susanna F.Nordström, Jakob

Search in DiVA

By author/editor
de Rezende, Susanna F.Nordström, Jakob
By organisation
School of Electrical Engineering and Computer Science (EECS)
Discrete Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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