Lower Bounds for Cutting Plane Logics via Communication Complexity
--- an introduction to communication methods in proof complexity

Proof complexity is a branch of computational complexity that studies the 
sizes of proofs of unsatisfiability in different systems of propositional 
logic.  The propositional proof systems studied arise as generalizations of 
classes of  algorithms for NP complete problems.   This talk focuses on 
the cutting planes logic that is based on the Gomory-cut method for solving integer programs.  This logic has also been implemented recently as the heart of so-called pseudo-boolean solvers for the SAT problem. 

We will show that there families of unsatisfiable CNFs on n variables,  of 
size poly(n), that require size 2^{O(n^\epsilon)} size refutations in 
cutting planes logic.   This is proved using by a reduction to the 
two-party communication complexity of the set-disjointness problem.

This talk is intended to be an accessible introduction to proof complexity 
and communication complexity for non-specialists.    The material in this 
talk is based on the work of  "Upper and Lower Bounds for Treelike Cutting 
Planes Lower Bounds" by Impagliazzo, Pitassi and Urquhart,  and  "Monotone Circuits for Matching  Require Linear Depth" by Raz and Wigderson.


Depending on interest, there may be a follow up talk discussing recent 
work of the speaker with Beame, Pitassi,  and Wigderson on extensions of 
this work relating to the Lovasz-Schrijver lift-and-project method of 
integer programming and multiparty number-on-the-forehead communcation.