Volume 16 (2020) Article 13 pp. 1-30
Monotone Circuit Lower Bounds from Resolution
by
Received: July 26, 2018
Revised: September 26, 2020
Published: November 9, 2020
Download article from ToC site:
[PDF (414K)]    [PS (2136K)]    [PS.GZ (468K)]
[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).