Tata Institute of Fundamental Research
Monotone Circuit Lower Bounds from Resolution
STCS Seminar
Speaker:
Pritish Kamath (Massachusetts Institute of Technology
Computer Science and Artificial Intelligence Lab.
The Stata Center, Building 32
32 Vassar Street
Cambridge, MA 02139
United States of America)
Organiser:
Ramprasad Saptharishi
Date:
Thursday, 28 Dec 2017, 14:00 to 15:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
It is well known that the communication complexity of the "(monotone) Karchmer-Wigderson game" corresponding to a boolean function exactly captures the depth (and hence size) of the smallest (monotone) *formula* computing the function. The DAG model of communication complexity generalizes this connection and exactly captures the size of the smallest (monotone) *circuit* computing the function!
In this work we show that for any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, a gadget-composed version of F requires large DAG communication protocols. By the above connection, this implies that a monotone function associated with F has large monotone circuit complexity. [Our result also extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.] (joint work with Ankit Garg, Mika Göös, Dmitry Sokolov. [ECCC TR17-175]).
| Speaker: | Pritish Kamath (Massachusetts Institute of Technology Computer Science and Artificial Intelligence Lab. The Stata Center, Building 32 32 Vassar Street Cambridge, MA 02139 United States of America) |
| Organiser: | Ramprasad Saptharishi |
| Date: | Thursday, 28 Dec 2017, 14:00 to 15:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
It is well known that the communication complexity of the "(monotone) Karchmer-Wigderson game" corresponding to a boolean function exactly captures the depth (and hence size) of the smallest (monotone) *formula* computing the function. The DAG model of communication complexity generalizes this connection and exactly captures the size of the smallest (monotone) *circuit* computing the function!
In this work we show that for any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, a gadget-composed version of F requires large DAG communication protocols. By the above connection, this implies that a monotone function associated with F has large monotone circuit complexity. [Our result also extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.] (joint work with Ankit Garg, Mika Göös, Dmitry Sokolov. [ECCC TR17-175]).
In this work we show that for any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, a gadget-composed version of F requires large DAG communication protocols. By the above connection, this implies that a monotone function associated with F has large monotone circuit complexity. [Our result also extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.] (joint work with Ankit Garg, Mika Göös, Dmitry Sokolov. [ECCC TR17-175]).