Christopher Beck

STOC Conference 2013 Conference Paper

Some trade-off results for polynomial calculus: extended abstract

• Christopher Beck
• Jakob Nordström
• Bangsheng Tang

We present size-space trade-offs for the polynomial calculus (PC) and polynomial calculus resolution (PCR) proof systems. These are the first true size-space trade-offs in any algebraic proof system, showing that size and space cannot be simultaneously optimized in these models. We achieve this by extending essentially all known size-space trade-offs for resolution to PC and PCR. As such, our results cover space complexity from constant all the way up to exponential and yield mostly superpolynomial or even exponential size blow-ups. Since the upper bounds in our trade-offs hold for resolution, our work shows that there are formulas for which adding algebraic reasoning on top of resolution does not improve the trade-off properties in any significant way. As byproducts of our analysis, we also obtain trade-offs between space and degree in PC and PCR exactly matching analogous results for space versus width in resolution, and strengthen the resolution trade-offs in [Beame, Beck, and Impagliazzo '12] to apply also to k-CNF formulas.

STOC Conference 2013 Conference Paper

Strong ETH holds for regular resolution

• Christopher Beck
• Russell Impagliazzo

FOCS Conference 2012 Conference Paper

Large Deviation Bounds for Decision Trees and Sampling Lower Bounds for AC0-Circuits

• Christopher Beck
• Russell Impagliazzo
• Shachar Lovett

There has been considerable interest lately in the complexity of distributions. Recently, Lovett and Viola (CCC 2011) showed that the statistical distance between a uniform distribution over a good code, and any distribution which can be efficiently sampled by a small bounded-depth AC0 circuit, is inverse-polynomially close to one. That is, such distributions are very far from each other. We strengthen their result, and show that the distance is in fact exponentially close to one. This allows us to strengthen the parameters in their application for data structure lower bounds for succinct data structures for codes. From a technical point of view, we develop new large deviation bounds for functions computed by small depth decision trees, which we then apply to obtain bounds for AC0 circuits via the switching lemma. We show that if such functions are Lipschitz on average in a certain sense, then they are in fact Lipschitz almost everywhere. This type of result falls into the extensive line of research which studies large deviation bounds for the sum of random variables, where while not independent, exhibit large deviation bounds similar to these obtained by independent random variables.

STOC Conference 2012 Conference Paper

Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space

• Paul Beame
• Christopher Beck
• Russell Impagliazzo

We give the first time-space tradeoff lower bounds for Resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size N that have Resolution refutations of space and size each roughly N log 2 N (and like all formulas have Resolution refutations of space N) for which any Resolution refutation using space S and length T requires T ≥ (N 0.58 log 2 N /S) Ω(log log N/log log log N) . By downward translation, a similar tradeoff applies to all smaller space bounds. We also show somewhat stronger time-space tradeoff lower bounds for Regular Resolution, which are also the first to apply to superlinear space. Namely, for any space bound S at most 2 o(N 1/4 ) there are formulas of size $N$, having clauses of width 4, that have Regular Resolution proofs of space S and slightly larger size T=O(NS), but for which any Regular Resolution proof of space S 1-ε requires length T Ω(log log N/ log log log N) .