pdf icon
Volume 16 (2020) Article 13 pp. 1-30
Monotone Circuit Lower Bounds from Resolution
Received: July 26, 2018
Revised: September 26, 2020
Published: November 9, 2020
Download article from ToC site:
[PDF (414K)] [PS (2136K)] [Source ZIP]
Keywords: circuit complexity, communication complexity, proof complexity
ACM Classification: F.1.3, F.2.3
AMS Classification: 68Q17, 68Q15, 03F20

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