How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
De Rezende, Susanna F. LU
; Nordstrom, Jakob
LU
and Vinyals, Marc
(2016)
57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016
In Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS
2016-December.
p.295-304
- Abstract
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 constantsize 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 [Krajǐcek '98], drawing on and extending techniques in [Raz and McKenzie... (More)
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 constantsize 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 [Krajǐcek '98], drawing on and extending techniques in [Raz and McKenzie '99] and [Ġoos 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-ACi1 and monotone-ACi, 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 logi n and polynomial size, but for which circuits of depth O(logi1 n) require exponential size.
(Less)
- author
- De Rezende, Susanna F.
LU
; Nordstrom, Jakob
LU
and Vinyals, Marc
- publishing date
- 2016-12-14
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Circuit complexity, Communication complexity, Cutting planes, Pebble games, Proof complexity, Trade-offs
- host publication
- Proceedings - 57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016
- series title
- Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS
- volume
- 2016-December
- article number
- 7782943
- pages
- 10 pages
- publisher
- IEEE - Institute of Electrical and Electronics Engineers Inc.
- conference name
- 57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016
- conference location
- New Brunswick, United States
- conference dates
- 2016-10-09 - 2016-10-11
- external identifiers
-
- scopus:85009372730
- ISSN
- 0272-5428
- ISBN
- 9781509039340
- 9781509039333
- DOI
- 10.1109/FOCS.2016.40
- language
- English
- LU publication?
- no
- id
- cf226f39-c678-4544-9daf-3ec13efa815d
- date added to LUP
- 2020-12-18 22:21:24
- date last changed
- 2024-08-06 02:59:45
@inproceedings{cf226f39-c678-4544-9daf-3ec13efa815d,
abstract = {{<p>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 constantsize 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 [Krajǐcek '98], drawing on and extending techniques in [Raz and McKenzie '99] and [Ġoos 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-ACi1 and monotone-ACi, 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 logi n and polynomial size, but for which circuits of depth O(logi1 n) require exponential size.</p>}},
author = {{De Rezende, Susanna F. and Nordstrom, Jakob and Vinyals, Marc}},
booktitle = {{Proceedings - 57th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2016}},
isbn = {{9781509039340}},
issn = {{0272-5428}},
keywords = {{Circuit complexity; Communication complexity; Cutting planes; Pebble games; Proof complexity; Trade-offs}},
language = {{eng}},
month = {{12}},
pages = {{295--304}},
publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
series = {{Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS}},
title = {{How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)}},
url = {{http://dx.doi.org/10.1109/FOCS.2016.40}},
doi = {{10.1109/FOCS.2016.40}},
volume = {{2016-December}},
year = {{2016}},
}