Hardness amplification in proof complexity

Abstract

We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems - tree resolution - into formulas that require large rank in very strong proof systems, including any proof system that manipulates polynomials of degree at most k (known as Th(k) proofs). These include high degree versions of Lovász-Schrijver and Cutting Planes proofs. We introduce two very general families of these proof systems, denoted 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 include Th(k-1) proofs as a special case. Rcc(k) proofs generalize Tcc(k) proofs and require only that each inference be checkable by a short k-party protocol. For all k ∈ O(loglog n), our main results are as follows: First, any unsatisfiable CNF formula of high resolution rank can be efficiently transformed into another CNF formula requiring high rank in all Rcc(k) systems, and exponential tree size in all Tcc(k) systems. Secondly, there are strict rank hierarchies for all Rcc(k) systems, and strict tree-size hierarchies for all Tcc(k) systems. Finally, we apply our general method to give optimal integrality gaps for low rank Rcc(2) proofs for MAX-2t-SAT, which imply optimal integrality gaps for low rank Cutting Planes and Th(1) proofs. © 2010 ACM.