ECCC-Report TR21-158https://eccc.weizmann.ac.il/report/2021/158Comments and Revisions published for TR21-158en-usThu, 25 Nov 2021 03:01:02 +0200
Revision 1
| Extremely Deep Proofs |
Noah Fleming,
Toniann Pitassi,
Robert Robere
https://eccc.weizmann.ac.il/report/2021/158#revision1We 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-epsilon}, 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-epsilon}/c must necessarily have depth approximately n^c. By setting c = o(n^{1-epsilon}) 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 [Razborov16]. Finally, we outline several conjectures that would imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting theorems.Thu, 25 Nov 2021 03:01:02 +0200https://eccc.weizmann.ac.il/report/2021/158#revision1
Paper TR21-158
| Extremely Deep Proofs |
Noah Fleming,
Toniann Pitassi,
Robert Robere
https://eccc.weizmann.ac.il/report/2021/158We 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-epsilon}, 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-epsilon}/c must necessarily have depth approximately n^c. By setting c = o(n^{1-epsilon}) 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 [Razborov16]. Finally, we outline several conjectures that would imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting theorems.Sun, 14 Nov 2021 04:27:35 +0200https://eccc.weizmann.ac.il/report/2021/158