Paul Beame
Trinh Huynh
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.
- R. Beals, H. Buhrman, R. Cleve, M. Mosca, and R. de Wolf. Quantum lower bounds by polynomials. JACM, 48(4):778--797, 2001. Google Scholar
Digital Library
- P. Beame, T. Pitassi, and N. Segerlind. Lower bounds for Lovasz-Schrijver systems and beyond follow from multiparty communication complexity. SIAM J. Comput., 37(3):845--869, 2007. Google ScholarDigital Library
- P. Beame and D.--T. Huynh--Ngoc. Multiparty communication complexity and threshold circuit size of AC0. In 50th IEEE FOCS, 53--62, 2009. Google ScholarDigital Library
- E. Ben-Sasson and A. Wigderson. Short proofs are narrow -- resolution made simple. JACM, 48(2):149--169, 2001. Google ScholarDigital Library
- J. Buresh-Oppenheim, N. Galesi, S. Hoory, A. Magen, and T. Pitassi. Rank bounds and integrality gaps for cutting planes procedures. In 44th IEEE FOCS, 318--327, 2003. Google ScholarDigital Library
- J. Buresh-Oppenheim and R. Santhanam. Making hard problems harder. TR06-03, ECCC, 2006.Google Scholar
- M. Charikar, K. Makarychev, and Y. Makarychev. Integrality gaps for Sherali-Adams relaxations. In 41st ACM STOC, 283--292, 2009. Google ScholarDigital Library
- A. Chattopadhyay and A. Ada. Multiparty communication complexity of disjointness. TR08-002, ECCC, 2008.Google Scholar
- V. Chvatal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics, 4:305--337, 1973.Google ScholarDigital Library
- V. Chvatal and Endre Szemeredi. Many hard examples for resolution. JACM, 35(4):759--768, 1988. Google ScholarDigital Library
- M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. CACM, 5:394--397, 1962. Google ScholarDigital Library
- J. Edmonds, R. Impagliazzo, S. Rudich, and J. Sgall. Communication complexity towards lower bounds on circuit depth. Computational Complexity, 10:210--246, 2001.Google ScholarCross Ref
- K. Georgiou, A. Magen, T. Pitassi, and I. Tourlakis. Integrality gaps of 2-o(1) for vertex cover SDPs in the Lovasz-Schrijver hierarchy. In 48th IEEE FOCS, 702--712, 2007. Google ScholarDigital Library
- R.E. Gomory. Outline of an algorithm for integer solutions to linear programs. Bull. of the AMS, 64:275--278, 1958.Google ScholarCross Ref
- D. Grigoriev. Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. TCS, 259:613--622, 2001.Google ScholarCross Ref
- D. Grigoriev, E. A. Hirsch, and D. V. Pasechnik. Complexity of semi-algebraic proofs. In STACS LNCS v. 2285, 419--430, 2002. Google ScholarDigital Library
- R. Impagliazzo and R. Paturi. On the complexity of k-SAT. JCSS, 67:367--375, 2001. Google ScholarDigital Library
- R. Impagliazzo, T. Pitassi, and A. Urquhart. Upper and lower bounds on tree-like cutting planes proofs. In 9th IEEE LICS, 220--228, 1994.Google Scholar
- M. Karchmer, R. Raz, and A. Wigderson. Super-logarithmic depth lower bounds via direct sum in communication complexity. Computational Complexity, 5:191--204, 1995.Google ScholarCross Ref
- A. Kojevnikov and A. Itsykson. Lower bounds of static Lovasz-Schrijver calculus proofs for Tseitin tautologies. In 33rd ICALP, 323--334, 2006. Google ScholarDigital Library
- J. Krajicek. Discretely ordered modules as a first-order extension of the cutting planes proof system. JSL, 63(4):1582--1596, 1998.Google ScholarCross Ref
- E. Kushilevitz and N. Nisan. Communication Complexity. Cambridge University Press, 1997. Google ScholarDigital Library
- J.B. Lasserre. An explicit SDP relaxation for nonlinear 0-1 programs. In IPCO, LNCS v. 2081, 293--303, 2001. Google ScholarDigital Library
- T. Lee and A. Shraibman. Disjointness is hard in the multi-party number-on-the-forehead model. In 23rd IEEE CCC, 81--91, 2008. Google ScholarDigital Library
- L. Lovasz and A. Schrijver. Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optimization, 1(2):166--190, 1991.Google ScholarCross Ref
- A. Maciel and T. Pitassi. Lower bounds on constant-depth Frege proofs with mod connectives modulo a hardness conjecture. In 11th IEEE LICS, 189--200, 2006. Google ScholarDigital Library
- S. Muroga. Threshold logic and its applications. John Wiley & Sons, 1971.Google Scholar
- N. Nisan and M. Szegedy. On the degree of boolean functions as real polynomials. Computational Complexity, 4:301--314, 1994. Google ScholarDigital Library
- R. Raz and P. McKenzie. Separation of the monotone NC hierarchy. Combinatorica, 19(3):403--435, 1999.Google ScholarDigital Library
- G. Schoenebeck. Linear level Lasserre lower bounds for certain k-CSPs. In 49th IEEE FOCS, 593--602, 2008. Google ScholarDigital Library
- G. Schoenebeck, L. Trevisan, and M. Tulsiani. A linear round lower bound for Lovasz-Schrijver SDP relaxations of Vertex Cover. In 22nd IEEE CCC, 205--216, 2007. Google ScholarDigital Library
- N. Segerlind and T. Pitassi. Exponential lower bounds and integrality gaps for tree-like Lovasz-Schrijver procedures. In ACM-SIAM SODA, 355--364, 2009. Google ScholarDigital Library
- A. Sherali and W. Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero--one programming problems. SIAM J. Disc. Math., 3:411--430, 1990. Google ScholarDigital Library
- A. A. Sherstov. Separating AC0 from depth-2 majority circuits. In 39th ACM STOC, 294--301, 2007. Google ScholarDigital Library
- A. A. Sherstov. The pattern matrix method for lower bounds on quantum communication. In 40th ACM STOC, 85--94, 2008. Full version: CoRR, abs/0906.4291. Google ScholarDigital Library
- M. Tulsiani. CSP gaps and reductions in the Lasserre hierarchy. In 41st ACM STOC, 303--312, 2009. Google ScholarDigital Library
Index Terms
- Hardness amplification in proof complexity
Recommendations
Query complexity in errorless hardness amplification
APPROX'11/RANDOM'11: Proceedings of the 14th international workshop and 15th international conference on Approximation, randomization, and combinatorial optimization: algorithms and techniquesAn errorless circuit for a boolean function is one that outputs the correct answer or "don't know" on each input (and never outputs the wrong answer). The goal of errorless hardness amplification is to show that if f has no size s errorless circuit that ...
Nisan-Wigderson generators in proof complexity: new lower bounds
CCC '22: Proceedings of the 37th Computational Complexity ConferenceA map g : {0, 1}n → {0, 1}m (m > n) is a hard proof complexity generator for a proof system P iff for every string b ∈ {0, 1}m \ Rng(g), formula τb(g) naturally expressing b ∉ Rng(g) requires superpolynomial size P-proofs. One of the well-studied maps ...
Impossibility results on weakly black-box hardness amplification
FCT'07: Proceedings of the 16th international conference on Fundamentals of Computation TheoryWe study the task of hardness amplification which transforms a hard function into a harder one. It is known that in a high complexity class such as exponential time, one can convert worst-case hardness into average-case hardness. However, in a lower ...
Comments