Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

On the virtue of succinct proofs : Amplifying communication complexity hardness to time-space trade-offs in proof complexity

Huynh, Trinh and Nordstrom, Jakob LU (2012) 44th Annual ACM Symposium on Theory of Computing, STOC '12 In Proceedings of the Annual ACM Symposium on Theory of Computing p.233-247
Abstract

An active line of research in proof complexity over the last decade has been the study of proof space and trade-offs between size and space. Such questions were originally motivated by practical SAT solving, but have also led to the development of new theoretical concepts in proof complexity of intrinsic interest and to results establishing nontrivial relations between space and other proof complexity measures. By now, the resolution proof system is fairly well understood in this regard, as witnessed by a sequence of papers leading up to [Ben-Sasson and Nordstrom 2008, 2011] and [Beame, Beck, and Impagliazzo 2012]. However, for other relevant proof systems in the context of SAT solving, such as polynomial calculus (PC) and cutting... (More)

An active line of research in proof complexity over the last decade has been the study of proof space and trade-offs between size and space. Such questions were originally motivated by practical SAT solving, but have also led to the development of new theoretical concepts in proof complexity of intrinsic interest and to results establishing nontrivial relations between space and other proof complexity measures. By now, the resolution proof system is fairly well understood in this regard, as witnessed by a sequence of papers leading up to [Ben-Sasson and Nordstrom 2008, 2011] and [Beame, Beck, and Impagliazzo 2012]. However, for other relevant proof systems in the context of SAT solving, such as polynomial calculus (PC) and cutting planes (CP), very little has been known. Inspired by [BN08, BN11], we consider CNF encodings of so-called pebble games played on graphs and the approach of making such pebbling formulas harder by simple syntactic modifications. We use this paradigm of hardness amplification to make progress on the relatively longstanding open question of proving time-space trade-offs for PC and CP. Namely, we exhibit a family of modified pebbling formulas {F n} n ∞ such that: • The formulas F n have size Θ(n) and width O(1). • They have proofs in length O(n) in resolution, which generalize to both PC and CP. • Any refutation in CP or PCR (a generalization of PC) in length L and space s must satisfy s log L ≈ > 4√n. A crucial technical ingredient in these results is a new two-player communication complexity lower bound for composed search problems in terms of block sensitivity, a contribution that we believe to be of independent interest.

(Less)
Please use this url to cite or link to this publication:
author
and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
cutting planes, length, pcr, polynomial calculus, proof complexity, resolution, size, space, trade-offs
host publication
STOC '12 - Proceedings of the 2012 ACM Symposium on Theory of Computing
series title
Proceedings of the Annual ACM Symposium on Theory of Computing
pages
15 pages
publisher
Association for Computing Machinery (ACM)
conference name
44th Annual ACM Symposium on Theory of Computing, STOC '12
conference location
New York, NY, United States
conference dates
2012-05-19 - 2012-05-22
external identifiers
  • scopus:84862626028
ISSN
0737-8017
ISBN
9781450312455
DOI
10.1145/2213977.2214000
language
English
LU publication?
no
id
7a612cfc-5b4e-4dfc-bb81-d2a942b074ab
date added to LUP
2020-12-18 22:27:15
date last changed
2022-02-24 02:24:35
@inproceedings{7a612cfc-5b4e-4dfc-bb81-d2a942b074ab,
  abstract     = {{<p>An active line of research in proof complexity over the last decade has been the study of proof space and trade-offs between size and space. Such questions were originally motivated by practical SAT solving, but have also led to the development of new theoretical concepts in proof complexity of intrinsic interest and to results establishing nontrivial relations between space and other proof complexity measures. By now, the resolution proof system is fairly well understood in this regard, as witnessed by a sequence of papers leading up to [Ben-Sasson and Nordstrom 2008, 2011] and [Beame, Beck, and Impagliazzo 2012]. However, for other relevant proof systems in the context of SAT solving, such as polynomial calculus (PC) and cutting planes (CP), very little has been known. Inspired by [BN08, BN11], we consider CNF encodings of so-called pebble games played on graphs and the approach of making such pebbling formulas harder by simple syntactic modifications. We use this paradigm of hardness amplification to make progress on the relatively longstanding open question of proving time-space trade-offs for PC and CP. Namely, we exhibit a family of modified pebbling formulas {F <sub>n</sub>} <sub>n</sub> <sup>∞</sup> such that: • The formulas F <sub>n</sub> have size Θ(n) and width O(1). • They have proofs in length O(n) in resolution, which generalize to both PC and CP. • Any refutation in CP or PCR (a generalization of PC) in length L and space s must satisfy s log L <sub>≈</sub> <sup>&gt;</sup> 4√n. A crucial technical ingredient in these results is a new two-player communication complexity lower bound for composed search problems in terms of block sensitivity, a contribution that we believe to be of independent interest.</p>}},
  author       = {{Huynh, Trinh and Nordstrom, Jakob}},
  booktitle    = {{STOC '12 - Proceedings of the 2012 ACM Symposium on Theory of Computing}},
  isbn         = {{9781450312455}},
  issn         = {{0737-8017}},
  keywords     = {{cutting planes; length; pcr; polynomial calculus; proof complexity; resolution; size; space; trade-offs}},
  language     = {{eng}},
  pages        = {{233--247}},
  publisher    = {{Association for Computing Machinery (ACM)}},
  series       = {{Proceedings of the Annual ACM Symposium on Theory of Computing}},
  title        = {{On the virtue of succinct proofs : Amplifying communication complexity hardness to time-space trade-offs in proof complexity}},
  url          = {{http://dx.doi.org/10.1145/2213977.2214000}},
  doi          = {{10.1145/2213977.2214000}},
  year         = {{2012}},
}