| Description |
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 long 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 cutting planes and polynomial calculus. Specifically, we exhibit a family of formulas F_nsuch that:
- F_n has size Theta(n) and width O(1).
- F_n has a resolution refutation in length O(n) which generalizes to both CP and PC.
- For any refutation of F_n in CP or PCR (an extension of PC) in length L and space s it holds that s log L is at least (roughly) sqrt[4]{n}.
A crucial technical ingredient in our result 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.
|