Volume 16 (2020) Article 13 pp. 1-30
Monotone Circuit Lower Bounds from Resolution
by
Revised: September 26, 2020
Published: November 9, 2020
For any unsatisfiable CNF formula $F$ that is hard to refute in the Resolution proof system, we show that a gadget-composed version of $F$ is hard to refute in any proof system whose lines are computed by efficient communication protocols—or, equivalently, that a monotone function associated with $F$ has large monotone circuit complexity. Our result extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.