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
How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-8923-1240
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-1487-445X
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. Vol. 2016, p. 295-304
Series
Annual IEEE Symposium on Foundations of Computer Science, ISSN 0272-5428 ; 2016
Keywords [en]
proof complexity, communication complexity, circuit complexity, cutting planes, trade-offs, pebble games
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-200426DOI: 10.1109/FOCS.2016.40ISI: 000391198500032Scopus ID: 2-s2.0-85009372730ISBN: 978-1-5090-3933-3 (print)OAI: oai:DiVA.org:kth-200426DiVA, id: diva2:1069716
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: 2018-01-13Bibliographically approved
In thesis
1. Space in Proof Complexity
Open this publication in new window or tab >>Space in Proof Complexity
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

ropositional proof complexity is the study of the resources that are needed to prove formulas in propositional logic. In this thesis we are concerned with the size and space of proofs, and in particular with the latter.

Different approaches to reasoning are captured by corresponding proof systems. The simplest and most well studied proof system is resolution, and we try to get our understanding of other proof systems closer to that of resolution.

In resolution we can prove a space lower bound just by showing that any proof must have a large clause. We prove a similar relation between resolution width and polynomial calculus space that lets us derive space lower bounds, and we use it to separate degree and space.

For cutting planes we show length-space trade-offs. This is, there are formulas that have a proof in small space and a proof in small length, but there is no proof that can optimize both measures at the same time.

We introduce a new measure of space, cumulative space, that accounts for the space used throughout a proof rather than only its maximum. This is exploratory work, but we can also prove new results for the usual space measure.

We define a new proof system that aims to capture the power of current SAT solvers, and we show a landscape of length-space trade-offs comparable to those in resolution.

To prove these results we build and use tools from other areas of computational complexity. One area is pebble games, very simple computational models that are useful for modelling space. In addition to results with applications to proof complexity, we show that pebble game cost is PSPACE-hard to approximate.

Another area is communication complexity, the study of the amount of communication that is needed to solve a problem when its description is shared by multiple parties. We prove a simulation theorem that relates the query complexity of a function with the communication complexity of a composed function.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2017. p. 318
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:15
Keywords
proof complexity, resolution, polynomial calculus, cutting planes, space complexity, computational complexity, pebble games, communication complexity, CDCL
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-206571 (URN)978-91-7729-422-1 (ISBN)
Public defence
2017-06-09, E2, Lindstedtsvägen, 3, Stockholm, 14:00 (English)
Opponent
Supervisors
Funder
EU, FP7, Seventh Framework Programme, 279611
Note

QC 20170509

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

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
de Rezende, Susanna F.Nordström, JakobVinyals, Marc
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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