Exponential lower bound for static semi-algebraic proofs

Abstract

Semi-algebraic proof systems were introduced in [1] as extensions of Lovász-Schrijver proof systems [2,3].These systems are very strong; in particular, they have short proofs of Tseitin's tautologies, the pigeonhole principle, the symmetric knapsack problem and the cliquecoloring tautologies [1]. In this paper we study static versions of these systems.W e prove an exponential lower bound on the length of proofs in one such system.The same bound for two tree-like (dynamic) systems follows.The proof is based on a lower bound on the "Boolean degree" of Positivstellensatz Calculus refutations of the symmetric knapsack problem. © 2002 Springer-Verlag Berlin Heidelberg.