Some of the most powerful techniques for solving NP-complete problems are based on integer programming techniques such as the Lovasz-Schrijver lift-and-project method. When used for satisfiability algorithms, such techniques can be viewed as propositional proof systems that prove tautologies (by establishing that the negation of a formula is unsatisfiable), and the proof structure is a successive derivation of low-degree inequalities over the rationals until a contradiction is found.
A major challenge on the frontier of propositional proof complexity is to understand the power of these propositional proof systems (which we call "threshold logics") . At present, it is conceivable that such systems could prove every tautology with derivation cubic in the size of the tautology (note: it is fairly easy to come up with examples that require large refutations by a particular algorithm based on these ILP techniques, however, the proof systems can be viewed as generalizations that nondeterministically make optimal choices at each step to minimize derivation size, so the difference is between proving lower bounds for a particular algorithm and proving lower bounds for all possible algorithms of a certain form). It is conjectured that there are tautologies which require exponential size to prove in these systems but there is yet no proof to confirm this.
In this lecture, we survey recent progress in a program towards proving size lower bounds for these logics by proving lower bounds for the multiparty number-on-the-forehead communication complexity of the set-disjointness function. Our primary contributions are: establishing the reduction from proof size lower bounds to communication lower bounds, and new lower bounds (that fall slightly short of what is needed for a superpolynomial proof size lower bound) for the NOF communication complexity of the set disjointness function.
Some of this material will appear in Computational Complexity 2005, some of it is submitted, and some of it is ongoing. Collaborators include Paul Beame, Toniann Pitassi, and Avi Wigderson.