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.

Authors

• Ankit Garg 0001
• Mika Göös
• Pritish Kamath
• Dmitry Sokolov 0001

Keywords

• Circuit complexity
• proof complexity