Robert Robere, DIMACS

Abstract

A recent line of work in complexity theory ("lifting theorems") analyze lower bounds in communication complexity by reducing them to lower bounds in query complexity, which is usually a much easier task. These techniques have proven to be very powerful, resolving a number of open problems. Further, due to known connections between communication complexity and circuit complexity, these tools have yielded new perspectives on proving circuit lower bounds, and have (so far) been extremely successful in resolving a number of open problems in monotone circuit complexity and proof complexity.

In this work, we strongly generalize an existing lifting theorem that reduces monotone span program lower bounds --- which is a circuit complexity measure --- to Nullstellensatz degree lower bounds --- which is a proof complexity measure. We apply our new lifting theorem to resolve several open problems in proof complexity and monotone circuit complexity, including:

• the first formal separation between Cutting Planes proofs with exponentially large coefficients and Cutting Planes proofs with polynomially bounded coefficients;
• the first exponential-size separation between Tree-Like Cutting planes with exponentially large coefficients and Tree-Like Cutting Planes with polynomially bounded coefficients; and
• the first exponential-size separation between monotone Boolean formulas and monotone real formulas, where the latter is a circuit model introduced by Krajicek that has played a key role in proof complexity.

This is joint work with Susanna de Rezende, Or Meir, Jakob Nordstrom, Toniann Pitassi, and Marc Vinyals.