Hardness Amplification in Proof Complexity

We present a generic method for converting any family of unsatisfiable CNF formulas that require large resolution rank into CNF formulas whose refutation requires large rank for proof systems that manipulate polynomials or polynomial threshold functions of degree at most k. (The latter are known as Th(k) proofs.) As special cases, such systems include: Lov?asz-Schrijver systems (LS, LS+), high degree analogues of Lov?asz-Schrijver (LS(k), LS+(k)), Cutting Planes and high degree versions of Cutting Planes (CP(k)), as well as Sherali-Adams and Lasserre proofs. We introduce two very general families of proof systems, denoted by Tcc (k) and Rcc (k). The proof lines of Tcc (k) are arbitrary Boolean functions, each of which can be evaluated by an efficient k-party randomized communication protocol. Tcc (k) proofs are very powerful and include Th(k - 1) proofs as a special case. Rcc (k) proofs generalize Tcc (k) proofs and require only that each inference be checkable (in a certain weak sens...

• Type: Conference
• Year: 2010
• Where: STOC
• Authors: Paul Beame, Trinh Huynh and Toniann Pitassi
• Keywords: Algorithms, Large Resolution Rank, Proofs Generalize Tcc, Rank Lower Bounds, STOC 2010