Revised: September 26, 2020
Published: November 9, 2020
Abstract: [Plain Text Version]
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.
An extended abstract of this paper appeared in the Proceedings of the 50th Symposium on Theory of Computing (STOC'18).