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
Lower Bounds and Trade-offs in Proof Complexity
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-8923-1240
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 [en]
Proof complexity, trade-offs, lower bounds, size, length, space
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-249610ISBN: 978-91-7873-191-6 (print)OAI: oai:DiVA.org:kth-249610DiVA, id: diva2:1318061
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
List of papers
1. Clique Is Hard on Average for Regular Resolution
Open this publication in new window or tab >>Clique Is Hard on Average for Regular Resolution
Show others...
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
Keywords
Proof complexity, regular resolution, k-clique, Erdos-Renyi random graphs
National Category
Discrete Mathematics
Identifiers
urn:nbn:se:kth:diva-244573 (URN)10.1145/3188745.3188856 (DOI)000458175600074 ()2-s2.0-85043471352 (Scopus ID)
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
2. How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
Open this publication in new window or tab >>How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
2016 (English)In: 2016 IEEE 57th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society, 2016, Vol. 2016, p. 295-304Conference paper, Published paper (Refereed)
Abstract [en]

We obtain the first true size-space trade-offs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constant-size coefficients, and the lower bounds apply to length and formula space (i.e., number of inequalities in memory) even for derivations with exponentially large coefficients. These are also the first trade-offs to hold uniformly for resolution, polynomial calculus and cutting planes, thus capturing the main methods of reasoning used in current state-of-the-art SAT solvers. We prove our results by a reduction to communication lower bounds in a round-efficient version of the real communication model of [Krajicek ' 98], drawing on and extending techniques in [Raz and McKenzie ' 99] and [Goos et al. '15]. The communication lower bounds are in turn established by a reduction to trade-offs between cost and number of rounds in the game of [Dymond and Tompa '85] played on directed acyclic graphs. As a by-product of the techniques developed to show these proof complexity trade-off results, we also obtain an exponential separation between monotone-AC(i-1) and monotone-AC(i), improving exponentially over the superpolynomial separation in [Raz and McKenzie ' 99]. That is, we give an explicit Boolean function that can be computed by monotone Boolean circuits of depth log(i) n and polynomial size, but for which circuits of depth O (log(i-1) n) require exponential size.

Place, publisher, year, edition, pages
IEEE Computer Society, 2016
Series
Annual IEEE Symposium on Foundations of Computer Science, ISSN 0272-5428 ; 2016
Keywords
proof complexity, communication complexity, circuit complexity, cutting planes, trade-offs, pebble games
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-200426 (URN)10.1109/FOCS.2016.40 (DOI)000391198500032 ()2-s2.0-85009372730 (Scopus ID)978-1-5090-3933-3 (ISBN)
Conference
57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016, New Brunswick, United States, 9 October 2016 through 11 October 2016
Note

QC 20170130

Available from: 2017-01-30 Created: 2017-01-27 Last updated: 2019-05-24Bibliographically approved
3. Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
Open this publication in new window or tab >>Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
Show others...
(English)Manuscript (preprint) (Other academic)
Abstract [en]

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:

  • We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomialline space if coefficients are restricted to be of polynomial magnitude.
  • We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.

An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-249607 (URN)
Note

QC 20190529

Available from: 2019-04-12 Created: 2019-04-12 Last updated: 2019-05-29Bibliographically approved
4. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling
Open this publication in new window or tab >>Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling
2019 (English)In: Proceedings of the 34th Annual Computational Complexity Conference (CCC ’19), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2019, Vol. 137, p. 18:1-18:16Conference paper, Published paper (Refereed)
Abstract [en]

We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if an only if there is a Nullstellensatz refutation of the pebbling formula over G in size t + 1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019
Series
Leibniz International Proceedings in Informatics, LIPIcs, ISSN 1868-8969 ; 137
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-249609 (URN)10.4230/LIPIcs.CCC.2019.18 (DOI)2-s2.0-85070721193 (Scopus ID)9783959771160 (ISBN)
Conference
34th Computational Complexity Conference, CCC 2019; New Brunswick; United States; 18 July 2019 through 20 July 2019
Note

QC 20190527

Available from: 2019-04-12 Created: 2019-04-12 Last updated: 2019-10-28Bibliographically approved
5. Cumulative Space in Black-White Pebbling and Resolution
Open this publication in new window or tab >>Cumulative Space in Black-White Pebbling and Resolution
2017 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2017Conference paper, Published paper (Refereed)
Abstract [en]

We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko 2015] as a tool for obtaining results in cryptography. We consider instead the nondeterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10-15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström 2008, 2011], we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017
Keywords
Clause Space, Cumulative Space, Parallel Resolution, Pebble Game, Pebbling, Proof Complexity, Resolution, Space, Commerce, Optical resolving power, Economic and social effects
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-206582 (URN)10.4230/LIPIcs.ITCS.2017.38 (DOI)2-s2.0-85034241142 (Scopus ID)9783959770293 (ISBN)
Conference
8th Innovations in Theoretical Computer Science Conference (ITCS 2017), January 9-11, 2017, Berkeley, CA, USA
Note

QC 20170509

Available from: 2017-05-05 Created: 2017-05-05 Last updated: 2019-05-29Bibliographically approved

Open Access in DiVA

thesis-sfdr.pdf(1106 kB)96 downloads
File information
File name FULLTEXT01.pdfFile size 1106 kBChecksum SHA-512
3f345b6115d2bf6a1cc5fa23ff7bfa3e7d68088ea9b36d65592998c3f012338b8e3911bf2450e6340930a5659920a37a7253814aeaa614c3808933f9bd1bebdb
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
de Rezende, Susanna F.
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 96 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

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