LOWER BOUNDS ON STATIC LOVASZ-SCHRIJVER CALCULUS PROOFS FOR TSEITIN TAUTOLOGIES

摘要

An exponential lower bound on the size of static Lovdsz-Schrijver proofs of Tseitin tautologies is established. Several techniques, such as translating a static LS_+ proof into a Positivstellensatz proof, extracting a "good" expander out of a given graph by removing edges and vertices, and proving a linear lower bound on the degree of Positivstellensatz proofs for Tseitin tautologies, are used.