Proofs and Circuits: Connections via Interpolation and Lifting
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
Proves equivalence between DAG-like communication for the Karchmer–Wigderson game and circuit size, extracts a protocol from a resolution refutation, and uses lifting with an indexing gadget to reduce GPHP to Clique vs Coloring. The composition makes Bob build a K−1-colorable graph and Alice pick an M^3 vertices per pigeon clique so that any differing edge gives a falsified pigeonhole clause, yielding a protocol size lower bound size ≥ m^K and thus monotone circuit and proof-size lower bounds (matching known n^{Ω(k)} tradeoffs).
AI-written summary · about