eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-25
70:1
70:23
10.4230/LIPIcs.ITCS.2022.70
article
Extremely Deep Proofs
Fleming, Noah
1
2
Pitassi, Toniann
3
4
5
Robere, Robert
6
University of California, San Diego, CA, USA
Memorial University, Canada
University of Toronto, Canada
Columbia University, New York, NY, USA
IAS, Princeton, NJ, USA
McGill University, Montreal, Canada
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol215-itcs2022/LIPIcs.ITCS.2022.70/LIPIcs.ITCS.2022.70.pdf
Proof Complexity
Tradeoffs
Resolution
Cutting Planes