Monotone Circuit Lower Bounds from Resolution

Ramprasad Saptharishi
Thursday, 28 Dec 2017, 14:00 to 15:00
A-201 (STCS Seminar Room)
It is well known that the communication complexity of the "(monotone) Karchmer-Wigderson game" corresponding to a boolean function exactly captures the depth (and hence size) of the smallest (monotone) *formula* computing the function. The DAG model of communication complexity generalizes this connection and exactly captures the size of the smallest (monotone) *circuit* computing the function!
In this work we show that for any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, a gadget-composed version of F requires large DAG communication protocols. By the above connection, this implies that a monotone function associated with F has large monotone circuit complexity. [Our result also extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.] (joint work with Ankit Garg, Mika Göös, Dmitry Sokolov. [ECCC TR17-175]).