Paper Info
Title
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 Lovasz-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 in 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.
Year
DOI
Venue
2009
10.1145/1806689.1806703
Proceedings of the forty-second ACM symposium on Theory of computing
Keywords
DocType
ISSN
unsatisfiable cnf formula,denoted tcc,low rank,proof system,hardness amplification,high resolution rank,optimal integrality gap,strict rank hierarchy,communication complexity,large rank,high rank,general method,proof complexity
Journal
0737-8017
Citations 
PageRank 
References 
13
0.51
40
Authors
3
Name
Order
Citations
PageRank
Paul Beame12234176.07
Trinh Huynh2442.53
Toniann Pitassi32282155.18