Dimitry Sokolov (KTH) - Monotone Circuit Lower Bounds from Resolution

Return to Full Calendar
January 15, 2019 at 3:30pm - 4:30pm
Ryerson, 251
Event Audience:
Dimitry Sokolov

Speaker: Dimitry Sokolov Postdoctoral Scholar, KTH Royal Institute of Technology

Research interests:
Proof complexity, communication complexity, structural complexity, algorithms.

Abstract: Monotone Circuit Lower Bounds from Resolution

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.

As an application, we show that a monotone version of the XOR SAT function has exponential monotone circuit complexity. Since XOR-SAT is in NC^2, this improves qualitatively on the monotone vs. non-monotone separation of Tardos (1988). Another corollary is that monotone span programs can be exponentially more powerful than monotone circuits.

Host: Department of Computer Science & Mathematics Combinatorics & Theory Seminar

Type: talk