We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program sizedue to Pitassi and Robere (STOC 2018) so that it works for any gadget with high enough rank. This means, in particular, that it applies for lifts using equality or greater-than gadgets.

We apply our new theorem to resolve an open problem in proof complexity: We exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. To the best of our knowledge, this is the first theorem separating cutting planes with and without polynomial bounds on coefficients in any way.

An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. This implies that the Nullstellensatz degree is equal to both the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem up to an additive constant 1.

This is joint work with Or Meir, Jakob Nordström, Toniann Pitassi, and Marc Vinyals.