Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #4 to TR19-186 | 25th February 2020 14:22

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity

RSS-Feed




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: 103
Keywords: 


Abstract:

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.



Changes to previous version:

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


Revision #3 to TR19-186 | 25th February 2020 14:21

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity





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: 45
Keywords: 


Abstract:

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.



Changes to previous version:

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


Revision #2 to TR19-186 | 7th January 2020 15:12

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity





Revision #2
Authors: Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, Susanna F. de Rezende
Accepted on: 7th January 2020 15:12
Downloads: 97
Keywords: 


Abstract:

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.



Changes to previous version:

Updated affiliations.


Revision #1 to TR19-186 | 31st December 2019 18:53

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity





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: 133
Keywords: 


Abstract:

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.



Changes to previous version:

Added Marc Vinyals as an author.


Paper:

TR19-186 | 31st December 2019 18:38

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity


Abstract:

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.



ISSN 1433-8092 | Imprint