Revision #4 Authors: Susanna de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Marc Vinyals

Accepted on: 25th February 2020 14:22

Downloads: 466

Keywords:

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:

* We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients.

Specifically, 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.

* We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.

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$.

In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

Added Marc Vinyals again as an author, after he got removed by mistake.

Revision #3 Authors: Susanna de Rezende, Or Meir, Jakob Nordström, Robert Robere, Toniann Pitassi, Marc Vinyals

Accepted on: 25th February 2020 14:21

Downloads: 183

Keywords:

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:

* We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients.

Specifically, 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.

* We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.

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$.

In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

Added Marc Vinyals again as an author, after he got removed by mistake.

Revision #2 Authors: Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Susanna F. de Rezende

Accepted on: 7th January 2020 15:12

Downloads: 285

Keywords:

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:

* We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients.

Specifically, 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.

* We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.

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$.

In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

Updated affiliations.

Revision #1 Authors: Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Marc Vinyals, Susanna F. de Rezende

Accepted on: 31st December 2019 18:53

Downloads: 313

Keywords:

Specifically, 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.

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$.

In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

Added Marc Vinyals as an author.

TR19-186 Authors: Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Susanna de Rezende

Publication: 31st December 2019 18:41

Downloads: 449

Keywords:

Specifically, 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.

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$.

In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.