Lower bounds of static Lovász–Schrijver calculus proofs for Tseitin tautologies
Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part I, Tome 340 (2006), pp. 10-32 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

We prove an exponential lower bound on the size of static Lovász-Schrijver proofs of Tseitin tautologies. We use several techniques, namely, translating a static $LS_+$ proof into a Positivstellensatz proof of Grigoriev et al., extracting a “good” expander out of a given graph by removing edges and vertices of Alekhnovich et al., and proving linear lower bound on the degree of Positivstellensatz proofs for Tseitin tautologies.
@article{ZNSL_2006_340_a1,
     author = {D. M. Itsykson and A. A. Kojevnikov},
     title = {Lower bounds of static {Lov\'asz{\textendash}Schrijver} calculus proofs for {Tseitin} tautologies},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {10--32},
     year = {2006},
     volume = {340},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2006_340_a1/}
}
TY  - JOUR
AU  - D. M. Itsykson
AU  - A. A. Kojevnikov
TI  - Lower bounds of static Lovász–Schrijver calculus proofs for Tseitin tautologies
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2006
SP  - 10
EP  - 32
VL  - 340
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2006_340_a1/
LA  - ru
ID  - ZNSL_2006_340_a1
ER  - 
%0 Journal Article
%A D. M. Itsykson
%A A. A. Kojevnikov
%T Lower bounds of static Lovász–Schrijver calculus proofs for Tseitin tautologies
%J Zapiski Nauchnykh Seminarov POMI
%D 2006
%P 10-32
%V 340
%U http://geodesic.mathdoc.fr/item/ZNSL_2006_340_a1/
%G ru
%F ZNSL_2006_340_a1
D. M. Itsykson; A. A. Kojevnikov. Lower bounds of static Lovász–Schrijver calculus proofs for Tseitin tautologies. Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part I, Tome 340 (2006), pp. 10-32. http://geodesic.mathdoc.fr/item/ZNSL_2006_340_a1/

[1] M. Alekhnovich, E. A. Hirsch, and D. Itsykson, “Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas”, J. of Automated Reasoning, 35 (2005), 51–72 | DOI | MR | Zbl

[2] M. Alekhnovich and A. Razborov, “Lower bounds for polynomial calculus: non-binomial case”, Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science, FOCS'01, 2001, 190–199 | MR

[3] P. Beame, T. Pitassi, and N. Segerlind,, “Multiparty communication complexity and lower bounds for threshold logics”, Proceedings of the 32th Annual Colloquium on Automata, Languages, and Programming, ICALP'05, 2005, 1176–1188 | MR | Zbl

[4] V. Chvátal, “Edmonds polytopes and a hierarchy of combinatorial problems”, Discrete Mathematics, 4 (1973), 305–337 | DOI | MR | Zbl

[5] M. Clegg, J. Edmonds, R. Impagliazzo, “Using the Groebner basis algorithm to find proofs of unsatisfiability”, Proceedings of the 28th Annual ACM Symposium on Theory of Computing, ACM, New York, 1996, 174–183 | MR | Zbl

[6] S. A. Cook, R. A. Reckhow, “The relative efficiency of propositional proof systems”, J. of Symbolic Logic, 44 (1979), 36–50 | DOI | MR | Zbl

[7] W. Cook, C. R. Coullard, G. Turán, “On the complexity of cutting-plane proofs”, Discrete Appl. Math., 18 (1987), 25–38 | DOI | MR | Zbl

[8] I. Dinur, “The PCP theorem by gap amplification”, Proceedings of the 38th Annual ACM Theory of Computing, STOC'06, ACM, New York, 2006, 241–250 | MR

[9] R. E. Gomory, “An algorithm for integer solutions of linear programs”, Recent Advances in Mathematical Programming, eds. R. L. Graves and P. Wolfe, McGraw-Hill, 1963, 269–302 | MR

[10] D. Grigoriev, “Linear lower bound on degrees of {P}ositivstellensatz Calculus proofs for the Parity”, Theor. Comput. Sci., 259 (2001), 613–622 | DOI | MR | Zbl

[11] D. Grigoriev, E. A. Hirsch, “Algebraic proof systems over formulas”, Theor. Comput. Sci., 303 (2003), 83–102 | DOI | MR | Zbl

[12] D. Grigoriev, E. A. Hirsch, D. V. Pasechnik, “Complexity of semialgebraic proofs”, Moscow Math. J., 2 (2002), 647–679 | MR | Zbl

[13] D. Grigoriev, N. Vorobjov, “Complexity of Null- and Positivstellensatz proofs”, Ann. Pure Appl. Logic, 113 (2001), 153–160 | DOI | MR

[14] L. Lovász, “Stable sets and polynomials”, Discrete Math., 124 (1994), 137–153 | DOI | MR | Zbl

[15] L. Lovász, A. Schrijver, “Cones of matrices and set-functions and 0-1 optimization”, SIAM J. Optim., 1 (1991), 166–190 | DOI | MR | Zbl

[16] A. Lubotzky, R. Phillips, P. Sarnak, “Ramanujan graphs”, Combinatorica, 8 (1988), 261–277 | DOI | MR | Zbl

[17] R. Murty, “Ramanujan graphs”, J. of the Ramanujan Math. Soc., 18 (2003), 1–20 | MR

[18] P. Pudlák, “Lower bounds for resolution and cutting plane proofs and monotone computations”, J. Symb. Logic, 62 (1997), 981–998 | DOI | MR | Zbl

[19] O. Reingold, “Undirected st-connectivity in log-space”, Proceedings of the 370th Annual ACM Symposium on Theory of Computing, STOC'05, 2005, 376–385 | MR

[20] A. Urquhart, “Hard examples for resolution”, J. ACM, 34 (1987), 209–219 | DOI | MR | Zbl

[21] G. A. Margulis, “Yavnye konstruktsii rasshiritelei”, Problemy peredachi informatsii, 9:4 (1973), 71–80 | MR | Zbl

[22] G. S. Tseitin, “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zap. nauchn. semin. LOMI, 8, 1968, 234–259