Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Lifting with simple gadgets and applications to circuit and proof complexity

De Rezende, Susanna LU orcid ; Meir, Or ; Nordstrom, Jakob LU ; Pitassi, Toniann ; Robere, Robert and Vinyals, Marc (2020) 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020 In Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS 2020-November. p.24-30
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 three 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... (More)

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 three 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. •We give the strongest separation to-date between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomial-size monotone Boolean circuits, requires monotone Boolean formulas of size 2{Omega(n text{polylog}(n))}. 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. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144.

(Less)
Please use this url to cite or link to this publication:
author
; ; ; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
circuit complexity, communication complexity, cutting planes, pebble games, proof complexity, trade-offs
host publication
Proceedings - 2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020
series title
Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS
volume
2020-November
article number
9317963
pages
7 pages
publisher
IEEE Computer Society
conference name
61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020
conference location
Virtual, Durham, United States
conference dates
2020-11-16 - 2020-11-19
external identifiers
  • scopus:85100337762
ISSN
0272-5428
ISBN
978-1-7281-9622-0
9781728196213
DOI
10.1109/FOCS46700.2020.00011
language
English
LU publication?
yes
additional info
Funding Information: Or Meir was supported by the Israel Science Foundation (grant No. 1445/16). Toniann Pitassi was supported by NSERC. Susanna F. de Rezende and Jakob Nordström were supported by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007–2013) / ERC grant agreement no. 279611, as well as by the Knut and Alice Wallenberg grant KAW 2016.0066. Susanna F. de Rezende also received funding fromg Knut and Alice Wallenberg Foundation grant KAW 2018.0371 and Jakob Nordström from the Swedish Research Council grants 621-2012-5645 and 2016-00782 and from the Independent Research Fund Denmark grant 9040-00389B. Part of this work was completed while Robert Robere was a postdoctoral researcher at DIMACS and the Institute for Advanced Study. This material is based upon work directly supported by the Charles Simonyi Endowment and indirectly supported by the National Science Foundation Grant No. CCF-1900460. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. Marc Vinyals was supported by the Prof. R Narasimhan post-doctoral award. Funding Information: Part of this work was carried out while several of the authors were visiting the Simons Institute for the Theory of Computing in association with the DIMACS/Simons Collaboration on Lower Bounds in Computational Complexity, which is conducted with support from the National Science Foundation. Publisher Copyright: © 2020 IEEE.
id
1d94d8bb-899a-455e-8ead-ef77ae35b69e
date added to LUP
2021-12-14 15:46:18
date last changed
2024-06-15 22:40:52
@inproceedings{1d94d8bb-899a-455e-8ead-ef77ae35b69e,
  abstract     = {{<p>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 three 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. •We give the strongest separation to-date between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomial-size monotone Boolean circuits, requires monotone Boolean formulas of size 2{Omega(n text{polylog}(n))}. 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. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144.</p>}},
  author       = {{De Rezende, Susanna and Meir, Or and Nordstrom, Jakob and Pitassi, Toniann and Robere, Robert and Vinyals, Marc}},
  booktitle    = {{Proceedings - 2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020}},
  isbn         = {{978-1-7281-9622-0}},
  issn         = {{0272-5428}},
  keywords     = {{circuit complexity; communication complexity; cutting planes; pebble games; proof complexity; trade-offs}},
  language     = {{eng}},
  pages        = {{24--30}},
  publisher    = {{IEEE Computer Society}},
  series       = {{Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS}},
  title        = {{Lifting with simple gadgets and applications to circuit and proof complexity}},
  url          = {{http://dx.doi.org/10.1109/FOCS46700.2020.00011}},
  doi          = {{10.1109/FOCS46700.2020.00011}},
  volume       = {{2020-November}},
  year         = {{2020}},
}