Volume 16 (2020) Article 13 pp. 1-30

Monotone Circuit Lower Bounds from Resolution

by Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov

Received: July 26, 2018
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.

--------------

An extended abstract of this paper appeared in the Proceedings of the 50th Symposium on Theory of Computing (STOC'18).

DOI: 10.4086/toc.2020.v016a013

© 2020 Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov
Licensed under a Creative Commons Attribution License (CC-BY)