License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITCS.2022.70
URN: urn:nbn:de:0030-drops-156665
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15666/
Go to the corresponding LIPIcs Volume Portal

Fleming, Noah ; Pitassi, Toniann ; Robere, Robert

Extremely Deep Proofs

pdf-format:
LIPIcs-ITCS-2022-70.pdf (0.8 MB)

Abstract

We further the study of supercritical tradeoffs in proof and circuit complexity, which is a type of tradeoff between complexity parameters where restricting one complexity parameter forces another to exceed its worst-case upper bound. In particular, we prove a new family of supercritical tradeoffs between depth and size for Resolution, Res(k), and Cutting Planes proofs. For each of these proof systems we construct, for each c ≤ n^{1-ε}, a formula with n^{O(c)} clauses and n variables that has a proof of size n^{O(c)} but in which any proof of size no more than roughly exponential in n^{1-ε}/c must necessarily have depth ≈ n^c. By setting c = o(n^{1-ε}) we therefore obtain exponential lower bounds on proof depth; this far exceeds the trivial worst-case upper bound of n. In doing so we give a simplified proof of a supercritical depth/width tradeoff for tree-like Resolution from [Alexander A. Razborov, 2016]. Finally, we outline several conjectures that would imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting theorems.

BibTeX - Entry

@InProceedings{fleming_et_al:LIPIcs.ITCS.2022.70,
  author =	{Fleming, Noah and Pitassi, Toniann and Robere, Robert},
  title =	{{Extremely Deep Proofs}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{70:1--70:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15666},
  URN =		{urn:nbn:de:0030-drops-156665},
  doi =		{10.4230/LIPIcs.ITCS.2022.70},
  annote =	{Keywords: Proof Complexity, Tradeoffs, Resolution, Cutting Planes}
}

Keywords: Proof Complexity, Tradeoffs, Resolution, Cutting Planes
Collection: 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)
Issue Date: 2022
Date of publication: 25.01.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI