Extremely Deep Proofs

on YouTube ↗28m

" summary

Proves that for resolution, k‑DNF resolution and cutting planes there are CNFs on n variables with polynomial‑size proofs but any subexponential‑size proof must have polynomial depth (a supercritical size–depth trade‑off); a smooth version gives formulas with size about 2^{n^δ} whose subexponential proofs require depth ≈2^{n^δ}. Method uses hardness condensation: start from pebbling formulas (small size, depth ≈N/log N), apply a xor gadget on an expanding bipartite graph to compress variables, and combine a depth‑condensation theorem with width→size lifting.

AI-written summary · about

" chapters (10)

1. 0:00Intro
2. 0:20A New Kind of Tradeoff Recently, several works exhibited an extremely strong type of tradeoff
3. 2:44Resolution Resolution: A method for proving that a CNF formula is unsatisfiable
4. 5:10Depth Like circuit depth, proof depth captures a notion of parallelism of a proof
5. 6:42This Work
6. 9:27Proof Technique Hardness Condensation
7. 10:46Lifting (Composition)
8. 19:53Depth Condensation Main workhorse behind our tradeoff
9. 22:03Main Tradeoff (For Resolution)
10. 22:44Supercritical Tradeoffs for Circuits