Monotone Circuit Lower Bounds from Resolution

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]).