Speaker: |
Jakob NordstrÃ¶m (KTH Royal Institute of Technology School of Computer Science and Communication SE-100 44 Stockholm SWEDEN) |

Organiser: |
Arkadev Chattopadhyay |

Date: |
Wednesday, 13 Mar 2013, 15:30 to 16:30 |

Venue: |
AG-69 |

(Scan to add to calendar)

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_n such 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.