Dima Grigoriev

AND Edward A Hirsch
email: hirsch@pdmi.ras.ru

Dmitrii V Pasechnik \mathematical

Yu I Manin

S A Cook

A R Reckhow

COMPLEXITY OF SEMI-ALGEBRAIC PROOFS

Keywords: 03F20; Secondary: 68Q17 1991 Mathematics Subject Classi cation, Computational complexity, propositional proof system, Extended

It is a known approach to translate propositional formulas into systems of polynomial inequalities and to consider proof systems for the latter ones. The well-studied proof systems of this kind are the Cutting Planes proof system (CP) utilizing linear inequalities and the Lovasz-Schrijver calculi (LS) utilizing quadratic inequalities. We introduce generalizations LS d of LS that operate with polynomial inequalities of degree at most d.

It turns out that the obtained proof systems are very strong. We construct polynomial-size bounded degree LS d proofs of the clique-coloring tautologies (which have no polynomial-size CP proofs), the symmetric knapsack problem (which has no bounded degree Positivstellensatz Calculus proofs), and Tseitin's tautologies (which are hard for many known proof systems). Extending our systems with a division rule yields a polynomial simulation of CP with polynomially bounded coe cients, while other extra rules further reduce the proof degrees for the aforementioned examples.

Finally, we prove lower bounds on Lov asz-Schrijverranks and on the \Boolean degree" of Positivstellensatz Calculus refutations. We use the latter bound to obtain an exponential lower bound on the size of static LS d and tree-like LS d refutations.

Introduction

An observation that a propositional formula can be written as a system of polynomial equations has lead to considering, in particular, the Nullstellensatz (NS) and the Polynomial Calculus (PC) proof systems, see Subsection 2.2 below (we do not dwell much here on the history of this rich area, one could nd several nice historical overviews in, e.g., BIK + 96, BIK + 97, Raz98, IPS99, CEI96, BGIP01]).

For these proof systems several interesting complexity lower bounds on the degrees of the derived polynomials were obtained Raz98, IPS99, BGIP01]. When the degree is close enough to linear (in fact, greater than the square root), these bounds imply exponential lower bounds on the proof complexity (more precisely, on the number of monomials in the derived polynomials) IPS99]. If polynomials are given by formulas rather than by sums of monomials as in NS or in PC, then the complexity could decrease signi cantly. Several gaps between these two kinds of proof systems were demonstrated in GH01].

Systems of polynomial inequalities yield much more powerful proof systems than these operating with equations only, such as NS or PC. The rst proof system working with inequalities was Cutting Planes (CP) Gom63, Chv73, CCT87, CCH89], see also Subsection 2.3. This system uses linear inequalities (with integer coe cients). Exponential lower bounds on proof size were established for CP with polynomially bounded coe cients BPR95] as well as for the general case Pud97].

Another family of well-studied proof systems are so-called Lov asz-Schrijver calculi (LS) LS91, Lov94], see also Pud99] and Subsection 2.3 below. In these systems one is allowed to deal with quadratic inequalities. No non-trivial complexity lower bounds are known for them so far. Moreover, generalizing LS to systems LS d that use inequalities of degree at most d (rather than 2 as in LS=LS 2 ) yields a very powerful proof system. In particular, there exists a short LS 4 proof of the clique-coloring tautologies (see Section 4). On the other hand, for these tautologies an exponential lower bound on the complexity of CP proofs was obtained in Pud97], relying on the lower bound for the monotone complexity Raz85]. Furthermore, we construct a short proof for the clique-coloring tautologies in the proof system LS + CP 2 (see Section 4) that manipulates just quadratic inequalities, endowed with the rounding rule (it generalizes directly the rounding rule for linear inequalities in CP). These results mean, in particular, that neither LS 4 nor LS + CP 2 have monotone e ective interpolation, while for a system LS + CP 1 where the use of rounding rule is limited to linear inequalities, a (non-monotone) e ective interpolation is known Pud99]. An analogue of (already mentioned) non-trivial lower bounds on the degree of derived polynomials in PC would fail in LS d as we show in Section 3, namely, every system of inequalities of degree at most d having no real solutions posseses an LS 2d refutation.

A proof system manipulating polynomialinequalities called the Positivstellensatz Calculus was introduced in GV01]. Lower bounds on the degree in this system were established for the parity principle, for Tseitin's tautologies Gri01b] and for the knapsack problem Gri01a]. Lower bounds on the Positivstellensatz Calculus degree are possible because its \dynamic" part is restricted to an ideal and an element of a cone is obtained from an element of ideal by adding the sum of squares to it. On the contrary, LS is a completely \dynamic" proof system. (The discussion on static and dynamic proof systems can be found in GV01]. Brie y, the di erence is that in LS a derivation constructs gradually an element of the cone generated by the input system of inequalities, while in the Positivstellensatz Calculus the sum of squares is given explicitly.) We consider a static version of Lov asz-Schrijver calculi and prove an exponential lower bound on the size of refutation of the symmetric knapsack problem (Section 9); this bound also translates into the bound for the tree-like version of (dynamic) LS. The key ingredient of the proof is a linear lower bound on the \Boolean degree" of Positivstellensatz Calculus refutations (Section 8). Note that exponential lower bounds on the size of (static!) Positivstellensatz refutations are still unknown.

Also the lower bound on the Positivstellensatz Calculus degree of the knapsack problem Gri01a] entails (see Subsection 7.2) a lower bound on the socalled LS-rank [START_REF] Lov | Stable sets and polynomials[END_REF][START_REF] Laurent | A comparison of the Sherali-Adams, Lov asz-Schrijver and Lasserre relaxations for 0-1 programming[END_REF]. Roughly speaking, the LS-rank counts the depth of multiplications invoked in a derivation. A series of lower bounds for various versions of the LS-rank were obtained in the context of optimization theory ST99, CD01, Das01, GT01]. For a counterpart notion in CP, the so-called Chv atal rank Chv73], lower bounds were established in CCT87, CCH89]. To the best of our knowledge, the connection between the Chv atal rank and CP proof complexity is not very well understood, despite a number of interesting recent results BEHS99, ES99]. As a rule, however, diverse versions of the rank grow at most linear, while we are looking for non-linear (exponential as a dream) lower bounds on the proof complexity. It turns out that for the latter purpose the rank is a too weak invariant. In particular, there are short proofs for the pigeon-hole principle (PHP) in CP CCT87] and in LS Pud97], while we exhibit in Subsection 7.3 a linear lower bound on the LS-rank of the PHP. Another example of this sort is supplied by the symmetric knapsack problem for which in Section 5 we give a short LS 3 -proof.

The above-mentioned LS 3 -proof of the symmetric knapsack follows from a general fact that LS d systems allow to reason about integers. In Section 6 we extend this technique to Tseitin's tautologies (which have no polynomial-size proofs in resolution Urq87], Polynomial Calculus BGIP01] and bounded-depth Frege systems BS02]). In Section 5 we also consider a certain extended version LS ;split of LS that, apart from the issue with integers, allows one to perform case analysis with respect to whether f > 0, f < 0, f = 0 for a linear function f (similar sorts of an extension of CP were introduced by Chv atal unpublished] Pud99] and Kraj cek Kra98]) and allows also to multiply inequalities. We show that LS ;split polynomially simulates CP with small coe cients. The same e ect can be achieved by replacing the multiplication and the case analysis by the division rule that derives g 0 from fg 0 and f > 0.

Finally, we formulate numerous open questions in Section 10.

Definitions

2.1. Proof systems. A proof system CR79] for a language L is a polynomial-time computable function mapping words (proof candidates) onto L (whose elements are considered as theorems). A propositional proof system is a proof system for any xed co-NP-complete language of Boolean tautologies (e.g., tautologies in DNF).

When we have two proof systems 1 and 2 for the same language L, we can compare them. We say that 1 polynomially simulates 2 , if there is a function g mapping proof candidates of 2 to proof candidates of 1 so that for every proof candidate for 2 , one has 1 (g( )) = 2 ( ) and g( ) is at most polynomially longer than .

Proof system 1 is exponentially separated from 2 , if there is an in nite sequence of words t 1 ; t 2 ; : : : 2 L such that the length of the shortest 1 -proof of t i is polynomial in the length of t i , and the length of the shortest 2 -proof of t i is exponential.

Proof system 1 is exponentially stronger than 2 , if 1 polynomially simulates 2 and is exponentially separated from it. When we have two proof systems for di erent languages L 1 and L 2 , we can also compare them if we x a reduction between these languages. However, it can be the case that the result of the comparison is more due to the reduction than to the systems themselves. Therefore, if we have propositional proof systems for languages L 1 and L 2 , and the intersection L = L 1 \ L 2 of these languages is co-NP-complete, we will compare these systems as systems1 for L.

Proof systems manipulating with polynomial equations.

There is a series of proof systems for languages consisting of unsolvable systems of polynomial equations. To transform such a proof system into a propositional proof system, one needs to translate Boolean tautologies into systems of polynomial equations.

To translate a formula F in k-DNF, we take its negation :F in k-CNF and translate each clause of :F into a polynomial equation. A clause containing variables v j1 ; : : :; v jt (t k) is translated into an equation (1 l 1 ) : : : (1 l t ) = 0; (2.1) where l i = v ji if variable v ji occurs positively in the clause, and l i = (1 v ji ) if it occurs negatively. For each variable v i , we also add the equation v2 i v i = 0 to this system.

Remark 2.1. Everywhere in this paper a polynomial is represented by deglex (or otherwise) ordered list of all its non-zero monomials. Observe that it does not make sense to consider our translation for formulas in general DNF (rather than k-DNF for constant k), because an exponential lower bound for any system using such encoding would be trivial (note that (1 v 1 )(1 v 2 ) : : :(1 v n ) denotes a polynomial with exponentially many monomials).

Note that F is a tautology if and only if the obtained system S of polynomial equations f 1 = 0, f 2 = 0, : : : , f m = 0 has no solutions. Therefore, to prove F it su ces to derive a contradiction from S.

Nullstellensatz (NS) BIK + 96]: A proof in this system is a collection of polynomials g 1 ; : : :; g m such that X i f i g i = 1: Polynomial Calculus (PC) CEI96]: This system has two derivation rules: p 1 = 0; p 2 = 0 p 1 + p 2 = 0 and p = 0 p q = 0 : (2.2) I.e., one can take a sum 2 of two already derived equations p 1 = 0 and p 2 = 0, or multiply an already derived equation p = 0 by an arbitrary polynomial q. The proof in this system is a derivation of 1 = 0 from S using these rules.

Positivstellensatz GV01]: A proof in this system consists of polynomials g 1 ; : : :; g m and h 1 ; : : :; h l such that X i f i g i = 1 + X j h 2 j (2.3) Positivstellensatz Calculus GV01]: A proof in this system consists of polynomials h 1 ; : : :; h l and a derivation of 1 + P j h 2 j = 0 from S using the rules (2.2). 2.3. Proof systems manipulating with inequalities. To de ne a propositional proof system manipulating with inequalities, we again translate each formula :F in CNF into a system S of linear inequalities, such that F is a tautology if and only if S has no 0-1 solutions. Given a Boolean formula in CNF, we translate each its clause containing variables v j1 ; : : :; v jt into the inequality l 1 + + l t 1; (2.4) where l i = v ji if the variable v ji occurs positively in the clause, and l i = 1 v ji if v ji occurs negatively. We also add to S the inequalities x 0; (2.5)

x 1 (2.6) for every variable x.

Cutting Planes (CP) Gom63, Chv73, CCT87, CCH89], cf. also Pud99]: In this proof system, the system S de ned above must be refuted (i.e., the contradiction 0 1 must be obtained) using the following two derivation rules: f 1 0; : : :; f t 0 P t i=1 i f i 0 (where i 0); (2.7) P i a i x i c P i a i x i dce (where a i 2 Z , and x i is a variable):

(2.8)

We restrict the intermediate inequalities in a CP derivation to the ones having integer coe cients (except the constant term).

Lov asz-Schrijver calculus (LS) LS91, Lov94], cf. also Pud99]: In the weakest of Lov asz-Schrijver proof systems, the contradiction must be obtained using the rule (2.7) applied to linear or quadratic f i 's and the rules f 0 fx 0 ; f 0 f(1 x) 0 (where f is linear, x is a variable): (2.9) Also, the system S is extended by the axioms x 2 x 0; x x 2 0 (2.10) for every variable x.

LS + LS91, Lov94, Pud99]: This system has the same axioms and derivation rules as LS, and also has the axiom l 2 0 (2.11) for every linear l.

LS LS91, Lov94, Pud99]: This system has the same axioms and derivation rules as LS, and also the derivation rule f 0; g 0 fg 0 (f; g are linear): (2.12) LS +; : This system unites LS + and LS . LS + CP 1 Pud99]: It has the same axioms and derivation rules as LS and also the rounding rule (2.8) of CP which can be applied only to linear inequalities. Note that all Lov asz-Schrijver systems described in this subsection deal either with linear or quadratic inequalities.

2.4. New dynamic systems. In this paper we consider several extensions of Lov asz and Schrijver proof systems. First, we de ne system LS + CP 2 which is slightly stronger than Pudl ak's LS + CP 1 . LS + CP 2 : It has the same axioms and rules as LS and also the extension of rounding rule (2.8) of CP to quadratic inequalities: P i;j a ij x i x j + P i a i x i c P i;j a ij x i x j + P i a i x i dce (where a i ; a ij 2 Z , and x i is a variable):

(2.13)

We then consider extensions of Lov asz-Schrijver proof systems allowing monomials of degree up to d.

LS d : This system is an extension of LS. The di erence is that rule (2.9) is now restricted to f of degree at most d 1 rather than to linear inequalities. Rule (2.7) can be applied to any collection of inequalities of degree at most d.

Remark 2.2. The degree d can be either 1 or a natural number greater than 1 (in the former case, the degree is unrestricted).

Remark 2.3. Note that LS=LS 2 .

Similarly, we consider LS d + , LS d and LS d +; , transforming in (2.11) (resp., (2.12)), the condition \l is linear" (resp., \f; g are linear") into \deg(l 2 ) d" (resp., \deg(fg) d").

LS d split : This system allows not only inequalities of the form f 0, but also of the form f > 0. The derivation rules (2.7) and (2.9) are extended in an obvious way to handle both types of inequalities, and f > 0 can be always relaxed to f 0. The axiom 1 > 0 is added. Also we allow to make assumptions of the form f > 0 and conclude f 0 if we can derive in LS d split a contradication from the assumption we made.

We now give a more formal de nition similar to Kraj i cek's R(CP) Kra98]. We consider the propositional fragment of (DAG-like) cut-free Gentzen style calculus with inequalities instead of Boolean formulas. We use one-sided sequents ! (where righthandside is treated for simplicity as multiset; in the following and denote arbitrary multisets) and derive contradiction (the empty sequent !) from the initial inequalities ! f i 0 taken from (2.4){(2.6), (2.10). In addition to a usual rule for working with sequents ! ! ;

(but not with Boolean connectives!), our derivation rules are: Static LS 1 : A proof in this system is a a refutation of a system of inequalities S = fs i 0g t i=1 , where each s i 0 is either an inequality given by the translation (2.4), an inequality of the form x j 0 or 1 x j 0, or an inequality of the form x 2 j x j 0. The refutation consists of positive real coe cients ! i;l and multisets U + i;l and U i;l de ning the polynomials u

! f > 0; f 0 (2.
i;l = ! i;l Y k2U + i;l x k Y k2U i;l (1 x k ) such that t X i=1 s i X l u i;l = 1: (2.16)
Static LS 1 + : The di erence from the previous system is that S is extended by inequalities s t+1 0; : : : ; s t 0 0, where each polynomial s j (j 2 t + 1::t 0 ]) is a square of another polynomial s 0 j . The requirement (2.16) transforms into

t 0 X i=1 s i X l u i;l = 1: (2.17)
Static LS + : The same as static LS 1 + , but the polynomials s 0 i can be only linear. Remark 2.6. Note that static LS + includes static LS 1 . Remark 2.7. Note that these static systems are not propositional proof systems in the sense of Cook and Reckhow CR79], but are something more general, since there is no clear way to verify (2.16) in deterministic polynomial time (cf. Pit97]). However, they can be easily augmented to match the de nition of Cook and Reckhow, e.g., by including a proof of the equality (2.16) or (2.17) using axioms of a ring (cf. F-NS of GH01]). Clearly, if we prove a lower bound for the original system, the lower bound will be valid for any augmented system as well.

Remark 2.8. The size of a refutation in these systems is the length of a reasonable bit representation of all polynomials u i;l , s i (for i 2 1::t]) and s 0 j (for j 2 t + 1::t 0 ]) and is thus at least the number of u i;l 's.

Example 2.1. We now present a very simple static LS + proof of the propositional pigeonhole principle. (It is easy to see that the same proof can be also conducted in (dynamic) LS + =LS 2 + ; there is even a polynomial-size (dynamic) LS proof Pud99], but it is slightly longer.) The negation of this tautology is given by the following system of inequalities (later denoted by PHP):

m 1 X `=1 x k` 1; 1 k m; (2.18) x k`+ x k 0 ` 1; 1 k < k 0 m; 1 ` m 1: (2.19
) (That says that the k-th pigeon must get into a hole, while two pigeons k and k 0 cannot share the same hole `.)

Here is the static LS

+ proof: m X k=1 m 1 X `=1 x k` 1 ! + m 1 X `=1 m X k=1 x k` 1 ! 2 + m 1 X `=1 m X k=1 m X k6 =k 0 =1 (1 x k` x k 0 `)x k`+ m 1 X `=1 m X k=1 (x 2 k` x k`) (m 1) = 1:
Known simulations and separations between semi-algebraic and other systems are given in Fig. 1 and2.

Encodings of formulas in LS d and upper bounds on the refutation degree

In LS d , Boolean formulas are encoded as linear inequalities. However, this is not the only possible way to encode them, since in LS d we can operate with polynomials of degree up to d. In particular, for formulas in k-CNF, one can use the same encoding as in Polynomial Calculus (2.1).

Consider system LS d that has the same derivation rules as LS d , but uses the encoding (2.1) instead of (2.4) (hence, this is a proof system for formulas in k-DNF for a constant k). It is clear that for d = 1, LS 1 polynomially simulates Polynomial Calculus. Does LS 1 polynomially simulate LS 1 (and Polynomial Calculus)? To give the positive answer, it su ces to show that there is a polynomial-size derivation of the encoding by polynomial equations from the encoding by linear inequalities. Lemma 3.1. There is a polynomial-size LS t derivation of (2.1) from (2.4), (2.5){ (2.10). ). The counterexample for CP (which provides the two separations in the middle) is given by the clique-coloring tautologies (resp., Theorem 4.1 and Pud97]). The two rightmost separations are due to Tseitin's formulas (resp., Theorem 6.1 and BS02]). Note that the knapsack problem is not a valid counterexample because it is not a translation of a formula in DNF.

Proof. We multiply (2.4) by (1 l 1 ), then by (1 l 2 ), : : : , (1 l t 1 ), eliminating terms l i (1 l i ) using (2.10) and (2.7) as soon as they appear. In this way, we obtain (1 l 1 ): : :(1 l t ) 0: The opposite inequality of (2.1) is trivial.

Corollary 3.1. For any d 2 f2; 3; : : : ; 1g, LS d polynomially simulates LS d (and, hence, LS 1 polynomially simulates Polynomial Calculus).

Corollary 3.2. LS 1 + polynomially simulates Positivstellensatz Calculus. Remark 3.1. Note that there is a linear lower bound Gri01a] on the degree of Positivstellensatz Calculus refutation of the symmetric knapsack problem m x 1 x 2 : : : x n = 0 (where m = 2 Z , m > dn=4e 2). However, by the completeness of LS LS91, Theorem 1.4] there is an LS (i.e., degree two) refutation of this problem.

It turns out that the converse of Lemma 3.1 is also true. In particular, that means that there is an LS k refutation of every unsatis able formula in k-CNF. Below, we also show (Theorem 3.1) that there is an LS 2k refutation of any system of polynomial inequalities of degree at most k. Lemma 3.2. There is a polynomial-size LS t derivation of (2.4) from (2.1) and

(2.5){(2.10). Proof. We derive (l 1 + : : : + l i 1)(1 l i+1 ) : : :(1 l t ) 0 (3.1) inductively. The base (i = 1) is trivial. Suppose that the inequality holds for i = m. Note that it can be rewritten as (l 1 + : : : + l m + l m+1 1 l 1 l m+1 : : : l m l m+1 )(1 l m+2 ) : : :(1 l t ) 0: We then add l j l m+1 (1 l m+2 ): : :(1 l t ) 0 (which easily follows from axioms) for j = 1; : : :; m obtaining (3.1) for i = m + 1.

Corollary 3.3. For any d 2 f2; 3; : : : ; 1g, LS d polynomially simulates LS d . Corollary 3.4. There is an LS k refutation of every formula in k-CNF. Theorem 3.1. There is an LS 2k refutation of any unsolvable system of polynomial inequalities of degree at most k. Proof. Consider an unsolvable system S of polynomial inequalities of degree at most k. We linearize it in the following way. Consider a monomial m = uvm 0 of degree at least two, where v and v are variables (it is possible that this is the same variable). Replace uv by a new variable x uv and add the following three inequalities to the system:

x uv u x uv v x uv u + v 1: Note that every 0-1 solution to the new system corresponds to a 0-1 solution to the old system, and vice versa. Therefore, the new system is unsolvable. Continue modifying the system in this way until it becomes a system S 0 of linear inequalities. Note that each new variable corresponds to a monomial in the old variables of degree at most k. We denote a variable corresponding to a monomial m by x m (note that x m may be not uniquely de ned, but it is not important for our argument). By LS91, Theorem 1.4], there is an LS (i.e., degree two) refutation of S 0 . For every added variable x m , replace x m by m in this refutation. We thus obtain a \proof" of S using only old variables.

We now must transform this \proof" into a valid LS 2k proof. The added inequalities become easily derivable from the axioms. The steps (2.7) remain valid steps. In (2.9), instead of multiplying by a new variable x u1u2:::us , we now multiply by the (old) variables u 1 ; u 2 ; : : :; u s .

We also have to replace steps (2.9) that use multiplying f 0 by (1 x u1u2:::us ). Instead, we multiply f 0 by (1 u 1 ), besides multiply f 0 by u 1 and by (1 u 2 ), besides multiply f 0 by u 1 , u 2 and (1 u 3 ), etc. Summing all the obtained inequalities, we get f(1 x u1u2:::us ) 0.

Since each added variable corresponds to a monomial of degree at most k, and the LS refutation of S 0 contains only monomials of degree at most two, we thus obtain a valid LS 2k refutation of the system S.

4. Short LS + CP 2 and LS 4 proofs of the clique-coloring tautologies Theorem 4.1. There is a set of inequalities that has polynomial-size refutations in LS 4 and LS + CP 2 , but has only exponential-size refutations in CP.

The set of inequalities we use is close to the one used by Pudl ak for proving an exponential lower bound for CP Pud97]. Pudl ak's bound remains valid for this system. Therefore, to achieve the result, we show that this set of inequalities has polynomial-size refutations in LS 4 and LS + CP 2 . Clique-coloring tautologies. Given a graph G with n vertices, we try to color it with m 1 colors, while assuming the existense of a clique of size m in G. Each edge (i; j) is represented by a (0-1) variable p ij . Variables q ki encode a (possibly multivalued) function from the integers f1 : : :mg denoting the vertices of a m-clique to the set f1 : : :ng of the vertices of G. Namely, q ki represents the i-th vertex of G being the k-th vertex of the clique. Variables r i`e ncode a (possibly multivalued) coloring of vertices by m 1 colors. The assignment of the color `to the node i is represented by a variable r i`.

The following inequalities Pud97] state that G has an m-clique and is (m 1)colorable. The correctness of coloring is expressed by p ij + r i`+ r j` 2; (4.1) where i, j and `satisfy 1 i < j n, `= 1 : : :m 1.

To make sure that each node gets colored, write

m 1 X `=1 r i` 1 (4.2)
for each i = 1 : : :n.

Then, every label of a clique is mapped to at least one vertex of G:

n X i=1 q ki 1 (4.3) for each k = 1 : : :m.
Also, the mapping encoded by q ki is injective: m X k=1 q ki 1 (4.4) for each i = 1 : : :n.

Finally, to encode that indeed one has a clique, write q ki + q k 0 ;j p ij + 1 (4.5) for all i, j, k, k 0 satisfying k 6 = k 0 and 1 i < j n.

Weak clique-coloring tautologies. The inequalities (4.1){(4.5) are the original inequalities of Pud97]. We now add one more family of inequalities to this system without a ecting applicability of Pud97, Corollary 7], that is, any CP refutation of the new system will still require at least 2 ((n=log n) 1=3 ) steps. Namely, we add n X i=1 q ki 1 (4.6) for all k = 1 : : :m. This inequality means that the k-th vertex of the clique does not get mapped to more than one vertex of G. PHP interpretation of weak clique-coloring tautologies. The fact that the i-th vertex of G is the k-th vertex of the clique and is colored with the color `is encoded as q ki r i` 1. Then the fact that the k-th vertex of the clique has color `is encoded as n X i=1 q ki r i` 1:

Let us denote this sum by x k`. Note that x k`' s de ne an injective (possibly multivalued) mapping from f1; : : : ; mg to f1; : : : ; m 1g. Below, we show that the PHP inequalities (2.18), (2.19) hold for x k`' s, furthermore, there are short LS 4 as well as LS + CP 2 derivations of these inequalities.

There is a polynomial-size CP refutation for PHP CCT87]. In our notation (note that x kl denotes a quadratic polynomial) such refutation translates into an LS+CP 2 refutation. Alternatively, Pudl ak Pud99] shows that PHP also has polynomial-size refutation in LS. In our notation, this translates into an LS 4 refutation. Note that both of these refutations make use of the following technical statement. Lemma 4.1. Given a sum of variables S = P N k=1 a k and inequalities a i + a j 1 for all 1 i < j N, there are short proofs of S 1 in LS and in CP. Proof. For CP, this is established in the proof of Proposition 7 in CCT87]. (It proceeds by induction: from a 1 + P i2F 1 and a 2 + P i2F 1 for F f1 : : :Ng f1; 2g one derives by summming these two inequalities and a 1 + a 2 1 that a 1 + a 2 + P i2F 3=2. The rounding down of the righthand side of the latter completes the proof of the induction step.)

For LS, this is Lemma 1 of Pud99], where the case N = 3 is dealt with, and an argument in the proof of Proposition 1 of [START_REF] Pudl | Lower bounds for resolution and cutting plane proofs and monotone computations[END_REF].

In what follows we show that there is a polynomial-size derivation of (2.18){(2.19) from (4.1){(4.6) in LS 4 as well as in LS + CP 2 . Deriving PHP from weak clique-coloring tautologies. Let us derive (2.18). For each i, multiply both sides of (4.2) by q ki and sum the resulting inequalities over i. One obtains

n X i=1 m 1 X `=1 q ki r i` n X i=1 q ki :
Adding (4.3) to this inequality, one gets (2.18).

Deriving (2.19) is less straighforward. First, we prove an easy lemma.

Lemma 4.2. In LS, there is a short proof of (a b) 2 0 for any variables a and b.

Proof. Multiplying both sides of a 1 by b, one obtains b 2 ab 0. Similarly, one derives a 2 ab 0. Summing the obtained two inequalities, one gets a 2 +b 2 2ab 0, as required.

Next, note that one can eliminate p ij from (4.1) and (4.5) and obtain q ki + q k 0 ;j + r i`+ r j` 3; 1 i < j n; 1 ` m 1; 1 k 6 = k 0 m: (4.7)

Using q 2 ki q ki and similar inequalities for q k 0 ;j , r i`a nd r j`, the inequality (4.7) can be rewritten as (q ki r i`) 2 + 2q ki r i`+ (q k 0 ;j r j`) 2 + 2q k 0 ;j r j` 3: Using Lemma 4.2, the latter is simpli ed to 2q ki r i`+ 2q k 0 ;j r j` 3: Applying the rounding rule, one obtains q ki r i`+ q k 0 ;j r j` 1 1 i < j n; 1 ` m 1; 1 k 6 = k 0 m:

(4.8)
Alternatively, we can derive (4.8) in LS 4 using the following lemma:

Lemma 4.3. In LS, there is a short proof that a + b 3=2 implies a + b 1.

Proof. Note that multiplying a 1 by 1 b gives a + b 1 + ab. It remains to show that ab 0. Indeed, multiplying a + b 3=2 by a (respectively, by 1 b) and using a = a 2 and b = b 2 one obtains ab a=2 0 (respectively, a ab 3=2 3=2b). Adding these two inequalities, one obtains a=2 + 3b=2 3=2. Multiplying the latter by b and using b 2 = b, one obtains ab 0.

Using q ki r i` q ki and (4.6), one obtains

(x k`= ) n X i=1
q ki r i` 1 1 ` m 1; 1 k m: (4.9) Now take (4.4) and add it to 0 q k 00 i for each k 00 di erent from k and k 0 . We get q ki + q k 0 i 1. After multiplying the latter inequality by r il and adding r il 1 to it, one obtains q ki r il + q k 0 i r il 1: (4.10) Now (4.8){(4.10) imply that any length 2 subsum of monomials in the sum S = n X i=1 (q ki r i`+ q k 0 i r i`) (for 1 k 6 = k 0 m) is bounded by 1 from above.

From these inequalities, one can easily derive S 1 either in LS 4 or in LS+CP 2 by using Lemma 4.1. As S = x k`+ x k 0 `, (2.19) holds, and we are done for LS+CP 2 .

For LS 4 it remains to show that all the x k`' s are boolean, as follows. Multiplying both sides of (4.9) by x k`, one obtains x 2 k` x k`. On the other hand, x 2 k`= x k`+ P i6 =j q ki r i`qkj r j` x k`h olds, as one can derive in LS 4 for each i and j that q ki r i`qkj r j` 0.

Reasoning about integers

In this section we explain how versions of Lov asz-Schrijver calculi can be used for reasoning about integers. In the following lemma the basic primitive for the latter, the family of quadratic inequalities f d (Y ) 0, is introduced. The lemma shows that there are short proofs of the fact that an integer linear combination of variables is either at most d 1 or at least d for any integer d. It follows then that there are short LS 3 (as well as LS ;0/1-split ) proofs of the symmetric knapsack problem, and that CP with polynomially bounded coe cients can be simulated in LS 3 = (as well as in LS ;split ). 1. LS 3 . 2. LS ;0/1-split .

Proof. W.l.o.g. rewrite Y as P t i=1 s i x li , where s i 2 f 1; 1g and it is possible that l i = l j . We derive the inequalities f c (Y j ) 0 inductively for Y j = P j i=1 s i x li and for each c 2 d t + j :: d + t j]. The base (j = 1) is trivial. Suppose that such inequalities are already derived for j k. We now derive (Y k+1 (c 1))(Y k+1 c) 0 for every c 2 d t + k + 1 :: d + t k 1]. 1. If s k+1 = 1, multiply f c 1 (Y k ) 0 by x k+1 , multiply f c (Y k ) 0 by (1 x k+1 ), and sum the obtained inequalities. We thus get in the left-hand side

f c 1 (Y k )x k+1 + f c (Y k )(1 x k+1 ) = (f c (Y k ) + 2(Y k (c 1)))x k+1 + f c (Y k )(1 x k+1 ) = f c (Y k ) + 2(Y k (c 1))x k+1 = Y 2 k ( 2c
1)Y k + c(c 1) + 2Y k x k+1 2(c 1)x k+1 : Using x 2 k+1 x k+1 = 0, we transform this into f c (Y k+1 ) which is (Y k + x k+1 ) 2 (2c 1)(Y k + x k+1 ) + c(c 1).

Else if s k+1 = 1, multiply f c+1 (Y k ) 0 by x k+1 , multiply f c (Y k ) 0 by (1 x k+1 ), and sum the obtained inequalities. We thus get in the left-hand side

f c+1 (Y k )x k+1 + f c (Y k )(1 x k+1 ) = (f c (Y k ) 2(Y k c))x k+1 + f c (Y k )(1 x k+1 ) = f c (Y k ) 2(Y k c)x k+1 = Y 2 k (2c 1)Y k + c(c 1) 2Y k x k+1 + 2cx k+1 : Using x 2 k+1 x k+1 = 0, we transform this into f c (Y k+1 ) which is in this case (Y k x k+1 ) 2 (2c 1)(Y k x k+1 ) + c(c 1).
2. The proof in LS ;0/1-split follows the proof in LS 3 given above. However, before multiplying by x k+1 and 1 x k+1 , we make an assumption x k+1 = r for r = 0; 1 (and thus multiply by constants, without increasing the degree). It is clear from the arguments above (just substitute the value for x k+1 ), that both assumptions lead to f c (Y k+1 ) 0 (which looks as f c (Y k ) 0 under assumption x k+1 = 0, as f c+1 (Y k ) 0 under assumption x k+1 = s k+1 and as f c 1 (Y k ) 0 under assumption x k+1 = s k+1 ).

Let us also note a general fact unrelated to integers: it is possible to substitute equalities into inequalities. Lemma 5.2. Let f be a polynomial in variables v 1 ; : : : ; v n , and X and Y be polynomials in variables v 2 ; : : : ; v n . Let g(v 2 ; : : : ; v n ) = f(X; v 2 ; : : :; v n ) and h(v 2 ; : : : ; v n ) = f(Y; v 2 ; : : :; v n ). Suppose that the degree of g and h is at most d. Then there is a polynomial-size LS d derivation of h 0 from g 0 and X Y = 0.

Proof. We rewrite g 0 as X i 1 (p i n i )X i + c 0;

(5.1) where p i and n i are polynomials of v 2 ; : : : ; v n consisting only of positive monomials, and c does not depend on X. Then we multiply Y X = 0 by p i (i.e., multiply it by its monomials and sum with the same coe cients as in p i ) and multiply X Y = 0 by n i . The sum of the obtained two equalities is (Y X)(p i n i ) = 0. We then multiply it by X i 1 , again representing it as a di erence of two polynomials containing only positive monomials. Summing (5.1) with the obtained equalities for every i, we get X i 2 ((p i n i )Y )X i 1 + (p 1 n 1 )Y + c 0:

We now represent (p i n i )Y as a di erence p 0 i n 0 i of two polynomials containing only positive monomials and repeat this procedure. Repeating it d times proves the claim.

It follows that there are short LS 3 (as well as LS ;0/1-split ) refutations of the symmetric knapsack problem.

Theorem 5.1. There is a polynomial-size LS 3 (as well as LS ;0/1-split ) refutation of m x 1 x 2 : : : x n = 0; (5.2) where m = 2 Z .

Proof. Using Lemma 5.2 substitute (5.2) into f bmc ( P n i=1 x i ) 0 given by Lemma 5.1.

To show that LS ;split and LS 3 = polynomially simulate CP, we rst (equivalently) rede ne CP so that it will manipulate linear inequalities of the form A a, where A = a 1 x 1 + : : : + a n x n , x 1 ; : : : ; x n are (integer) variables, and a 1 ; : : : ; a n ; a are integers. The rounding rule (2.8) transforms into P i a i x i a P i ai d x i d a d e (where d 2 N; dja 1 ; : : :; a n ):

(5.3)

We de ne CP with polynomially bounded coe cients (cf. BPR95]) if the absolute values of a i are bounded by a polynomial in the length of a CP refutation.

Theorem 5.2. The following systems polynomiallysimulate CP with polynomially bounded coe cients: 1. LS ;split . 2. LS 3 = . Proof. We x a CP refutation and simulate it rule by rule. Simulating the rule (2.7) goes literally in LS, so we need to simulate just the rule (5.3). By Lemma 5.1 we can derive in LS ;0/1-split (as well as in LS 3 ) the inequality f c (A=d) 0 for c = da=de. 1. In LS ;split , we then have that A=d c since the assumption A=d c < 0 multiplied by A=d (c 1) > 0 contradicts f c (A=d) 0.

2. In LS 3 = , we get A=d c by dividing f c (A=d) 0 by A=d (c 1) > 0.

Remark 5.1. In the proof of Theorem 5.2 the hypotheses f > 0, f 0 used for LS ;split derivations are just linear.

Short proof of Tseitin's tautologies in LS d

We recall the construction of Tseitin's tautologies. Let G = (V; E) be a graph with an odd number n of vertices. Attach to each edge e 2 E a Boolean variable x e , i.e. x 2 e = x e . The negation T = T G of Tseitin's tautologies with respect to G (see e.g., BGIP01, GH01]) is a family of formulas meaning that for each vertex v of G the sum P e3v x e ranging over the edges incident to v is odd. Clearly, T is contradictory.

In the applications to the proof theory BGIP01, Urq87] the construction of G is usually based on an expander. In particularly, G is d-regular, i.e., each vertex has degree d, where d is a constant. The respective negation T = T G of Tseitin's tautologies is given by the following equalities (due to Lemmas 3.1 and 3.2 we give them directly in PC translation):

Y e2S 0 v x e Y e= 2S 0 v
(1 x e ) = 0 (6.1) (for each vertex v and each subset S 0 v of even cardinality of the set S v of edges incident to v). There are 2 d 1 equalities of degree d for each vertex of G. Theorem 6.1. For every constant d 1 and every d-regular graph G, there is a polynomial-size refutation of (6.1) in LS d+2 . Proof. Denote Y i = y v1 + : : : + y vi , where v 1 ; : : : ; v i are pairwise distinct vertices of G and y v = P e3v x e . For every c 2 0 :: i(d 1)=2], we will prove inductively f c (Y i =2) 0 for odd i = n; n 2; n 4; : : : and f c ((Y i 1)=2) 0 for even i = n 1; n 3; : : :. Then f 0 ((Y 0 1)=2) 0 gives a contradiction.

The induction base (i = n) follows from Lemma 5.1, since Y n = 2 P e2E x e and therefore Y n =2 is an integer linear combination of variables.

To proceed from step i + 1 to step i of the refutation, denote Y = Y i+1 and y = P e3vi+1 x e . We assume for de niteness that i is odd (the case of an even i is treated in a similar way). We need to prove that f c ((Y y)=2) 0 for all c 2 0 :: i(d 1)=2].

Fix some subset S S vi+1 of odd size. Let t = jSj, c 0 = c + (t 1)=2 2 c :: c + (d 1)=2] 0 ::

(i + 1)(d 1)=2]. Denote P(S) = Q e2S x e Q e= 2S
(1 x e ). Since we have f c 0((Y 1)=2) 0 by the induction hypothesis, f c 0((Y 1)=2) P(S) 0 follows by (2.9), and can be rewritten as ((Y 1)=2 c 0 ) (((Y y)=2 (c 1))P(S) + (y=2 t=2)P(S)) 0: (6.2) Also yP(S) = tP(S) (6.3) follows directly from (2.10) and (2.9). Substituting (6.3) into (6.2) by Lemma 5.2 we get ((Y 1)=2 c 0 ) ((Y y)=2 (c 1)) P(S) 0 which can be rewritten as (((Y y)=2 c)P(S) + (y=2 t=2)P(S)) ((Y y)=2 (c 1)) 0 Substituting (6.3) again we get f c ((Y y)=2) P(S) 0: (6.4)

We complete induction step by summing (6.4) for all S S vi+1 of odd size. By Lemma 5.2, it remains then to prove that 1 = X S Sv jSj is odd

P(S)

This last equality is the sum of the equalities (6.1) for xed vertex v, because one can rewrite 1 = x + (1 x) = xy + (1 x)y + x(1 y) + (1 x)(1 y) = : : : for any collection of variables x; y; : : :. Remark 6.1. Sometimes Tseitin's tautologies are formulated in a di erent way.

One takes G with arbitrary (not necessarily odd) number of vertices, attaches weight w v 2 f0; 1g to each vertex v and writes Boolean formulas expressing L e3v x e = w v .

Then if L v2V w v = 1, this set of formulas is contradictory. Note that our technique works for this kind of Tseitin's tautologies as well. Remark 6.2 (A. Kojevnikov). The degree of proof of Tseitin's tautologies can be reduced by the use of the rounding rule (2.8) applied to higher degree inequalities. For example, there is a short proof of degree 6 tautologies in \ LS 6 + CP 3 " proof system. First, one notes that (y v 1)(y v 3)(y v 5) = 0 because it is an integer linear combination of the equalities (6.1). Then, one sums all the obtained equalities, getting 2c P e2E x e = 2k + 1 for certain integers c and k. Applying the rounding rule to each of the inequalities constituting this equality and summing the results gives a contradiction.

Lower bounds on Lov asz-Schrijver rank

In this section we prove two lower bounds on Lov asz-Schrijver rank. There is a series of lower bounds on Lov asz-Schrijver rank in the literature (see e.g. CD01, GT01] and the references there). However, these bounds are not suitable for the use in the propositional proof theory, because these are either bounds for solvable systems of inequalities, or bounds for systems with exponentially many inequalities.

We rst prove (Subsection 7.2) a linear lower bound on the LS + -rank (and a logarithmic lower bound on the LS +; -rank) of symmetric knapsack problem by reducing it to a lower bound on the degree of Positivstellensatz Calculus refutation Gri01a] (see also Theorem 8.1). However, this system of inequalities is not obtained as a translation of a propositional formula, and thus lower bounds for it cannot be directly used in the propositional proof theory.

Then in Subsection 7.3 we prove an (2 p n ) lower bound on the LS-rank of PHP. Note (cf. Subsection 2.5) that the LS + -rank of PHP is a constant. 7.1. More de nitions. We now consider the standard geometric setting for the Lov asz-Schrijver procedures LS and LS + LS91]. A comprehensive explanation of its equivalence with propositional proof complexity setting can be found in Das01].

Given a system Ax b of m linear inequalities in variables x 1 ; : : :; x n , we homogenize it by adding an extra variable x 0 and writing the system as x 0 0; Ax x 0 b: (7.1) Then let K denote the set of feasible points of (7.1) and K I denote the cone generated by all 0-1 vectors in K. Also, let Q denote the cone generated by the 0-1 vectors of length n + 1 with the rst coordinate equal to 1. In what follows, e j denotes j-th unit vector, and Diag(Y ) is the vector of the main diagonal entries of a square matrix Y . We write Y 0 if Y is positive semide nite.

The set M(K) (denoted usually M(K; Q), but this generality is not needed here) consists of (n + 1) (n + 1) real matrices Y satisfying (i) Y = Y T ;

(ii) Y e 0 = Diag(Y );

(iii) Y e i 2 K and Y (e 0 e i ) 2 K for all 0 i n. Also, de ne M + (K) := fY 2 M(K) j Y 0g.

Next, de ne the projections of M(K) and M + (K) onto R n+1 as follows.

N(K) := fDiag(Y ) j Y 2 M(K)g N + (K) := fDiag(Y ) j Y 2 M + (K)g: Iterated operators N r (K) and N r + (K) are de ned naturally as N 0 (+) (K) := K and N r (+) (K) := N (+) (N r 1 (+) (K)). It is shown in LS91] that

K I N n (+) (K) N n 1 (+) (K) N k (+) (K) N (+) (K) K: (7.2)
The LS-rank (respectively, LS + -rank) of a system of linear inequalities Ax b is the minimal k in (7.2) such that N k (K) = K I (respectively, N k + (K) = K I ), where K = K(A; b), as above.

Alternative de nitions of Lov asz-Schrijver ranks in proof systems terms are as follows. A proof in Lov asz-Schrijver proof system is a directed acyclic graph whose vertices correspond to the derived inequalities, and there is an edge between f 0 and g 0 i g is derived from f (and maybe something else) in one step. We now drop the edges corresponding to the rule (2.7). The rank of a refutation is the length of the longest path from an axiom to the contradiction in this graph. The LS -rank of a system is the smallest rank of an LS-refutation for it. The LS +rank is the smallest rank of an LS + -refutation. Similarly, one can de ne LS -and LS +; -ranks. Note that this de nition generalizes smoothly to LS d , LS d + , LS d and LS d +; . 7.2. LS + -and LS +; -ranks of symmetric knapsack. The system of inequalities for the symmetric knapsack problem is given by (5.2) and usual axioms (2.5), (2.6), (2.10). We restrict our attention to system K obtained by setting m = n 2 + 1 2 .

Theorem 7.1.

1. LS + -rank of K is at least n=4. 2. LS +; -rank of K is at least log 2 n 1. Proof. 1. Fix an LS + -refutation of K. We now modify it into a Positivstellensatz refutation (See Subsection 2.2).

For each polynomial f derived in LS + with LS + -rank at most k we construct its representation in the form f =

X i (x i x 2 i )u i + (m X i x i )u 0 + X j v 2 j (7.3)
in such a way that all the degrees deg(x i x 2 i )u i ; deg(m P i x i )u 0 ; deg v 2 j 2k (by recursion on k). Indeed, the recursive step is obvious for the rules (2.10), (2.11). Furthermore, we replace the rst rule of (2.9) by the multiplication by x = (x x 2 ) + x 2 providing the representation fx =

X (x i x 2 i )u i x + (x x 2 ) X v 2 j + (m X x i )u 0 x + X (v j x) 2 ;
that gives the form of fx similar to (7.3). Similarly, we replace the second rule of (2.9) by the multiplication by (1 x) = (x x 2 ) + (1 x) 2 . At the end of the derivation in LS + of LS + -rank k + we get a representation of the form 1 = X

(x i x 2 i )u i + (m X x i )u 0 + X v j 2
where deg(x i x 2 i )u i ; deg(m P x i )u 0 ; deg v j 2 2k + by recursion. This provides a Positivstellensatz Calculus refutation of the knapsack problem with the degree less or equal to 2k + . Applying Gri01a] (cf. also Theorem 8.1) we conclude that 2k + n=2, thus LS + -rank of K is at least n=4. 2. We x an LS +; -refutation of K and observe in a similar way that if two derived polynomials f and g = X (x i x 2 i )u 0 i + (m X x i )u 0 0 + X (v 0 j ) 2 of LS +; -rank at most k are already in the form (7.3) where deg

(x i x 2 i )u i ; deg(m X x i )u 0 ; deg v 2 j ; deg(x i x 2 i )u 0 i ; deg(m X x i )u 0 0 ; deg(v 0 j ) 2 2 k ; their product fg = X (x i x 2 i )u i g + X (x i x 2 i )u 0 i X v 2 j + (m X x i )u 0 g+ (m X x i )u 0 0 X v 2 j +
X (v j1 v 0 j2 ) 2 can be written again in the desired form (7.3) with the degrees of the occurring polynomials bounded by 2 k+1 . This allows one to replace the rule (2.12). By recursion at the end of the derivation in LS +; of the LS +; -rank k we get a representation 1 = X (x i x 2 i ) e u i + (m

X x i )f u 0 + X e v j 2
with the degrees deg(x i x 2 i ) e u i ; deg(m P x i )f u 0 ; deg e v j 2 2 k . Again as above applying Gri01a] (or Theorem 8.1) we conclude that 2 k n=2 and thereby, LS +;rank of K is at least log 2 n 1.

Remark 7.1. Similarly to Theorem 7.1(2), a logarithmic lower bound on the LS +; -rank can be obtained for the parity principle and for Tseitin's tautologies relying on Gri01b]. 7.3. LS-rank of PHP. Let e k denote all-1 vector of length k.

Let Q n R n denote the n-dimensional 0-1 hypercube and let P m 1 be the feasible set of the system (2.18)-(2.19). This is the well-known \PHP polytope". Theorem 7.2. At least m 2 iterations of the N-operator are needed to prove that P m 1 does not contain integer points, that is, LS-rank of P m 1 is at least m 2.

It will follow from Lemma 7.2 below.

Write x 2 Ñr (m 1) i (1; x) 2 N r (P m 1 ). We also identify Ñ0 (m 1) with P m 1 itself.

Let x 2 Ñ0 (m 1). De ne w ab = w ab (x) 2 Q m(m+1) , where 1 a m + 1, 1 b m, as follows.

w ab ij = 8 > > > > > > < > > > > > > : x i;j if 1 i < a; 1 j < b; x i;j 1 if 1 i < a; b < j m; x i 1;j if a < i m + 1; 1 j < b; x i 1;j 1 if a < i m + 1; b < j m; 1 if i = a; j = b; 0 otherwise.
Lemma 7.1. Let x 2 Ñr (m 1). Then w ab (x) 2 Ñr (m).

Proof. It is trivial to check the statement for r = 0.

We make an induction assumption that for any x and any t < r, x 2 Ñt (m 1) implies w ab (x) 2 Ñt (m). Without loss in generality, assume a = b = 1. We x a particular basis (e 1 ; : : :; e m(m 1) ) in R m(m 1) :

(x 1;1 : : :x 1;m 1 ; x 2;1 : : :x m;1 ; x 2;2 : : :x 2;m 1 ; x 3;2 : : :; x m;m 1 ): (it just gives a particularly nice ordering of variables for the purpose.) In such a basis, w 11 (x) = (1; 0 : : :0; x). Assume x 2 Ñr (m 1). Thus there exists Y = 1 x T x Y 0 2 M(N r 1 (P m 1 )).

De ne

Y = 0 B B @ 1 1 (0 : : :0) T x T 1 1 (0 : : :0) T x T
(0 : : :0) (0 : : :0) 0 2m 1;2m 1 0 2m 1;m(m 1)

x x 0 m(m 1);2m 1

Y 0 1 C C A ;
where 0 s;q denotes the all-0 matrix of size s q. We show that Y 2 M(N r 1 (P m )), implying the statement of the lemma.

By construction, Y T = Y , Y 0;j = Y jj and Y 0;j = Y jj . Note that if Y 0;j = 0 then Y e j = 0, as P m 1 Q m(m 1) . Hence Y 0;j = 0 implies Y e j = 0. Thus if Y e j 6 = 0 then we can normalize 1 Y 0;j Y e j . Hence, by induction assumption applied to x = Y e j , one has 1 Y 0;j Y e j 2 N r 1 (P m ) for all j such that Y 0;j 6 = 0. Hence Y e j 2 N r 1 (P m ) for all j.

Similarly, as any nonzero vector of the form Y (e 0 e k ) satis es Y (e 0 e k ) 0 = 1 Y 0;k > 0, normalizing a nonzero Y (e 0 e j ) with its 0-th coordinate, one obtains, for j > 0, that either Y (e 0 e j ) = 0 or 1 1 Y 0;j Y (e 0 e j ) 2 N r 1 (P m ). Hence Y (e 0 e j ) 2 N r 1 (P m ) for all j > 0.

Lemma 7.2. 1

m 1 e m(m 1) 2 Ñm 3 (m 1) for m 3.

Proof. Trivial for m = 3. Denote x k = 1 k e k(k+1) . By induction, assume x k 2 Ñk 2 (k) for all 1 < k < m 1. Set the matrix Y to have columns (1; x m 1 ), 1 m 1 (1; w 11 (x m 2 )), 1 m 1 (1; w 12 (x m 2 )), : : : , 1 m 1 (1; w m;m 1 (x m 2 )). Then Y T = Y , Y 0;j = Y jj .

By induction assumption and Lemma 7.1, Y e j 2 N m 4 (P m 1 ) for each j > 0.

Next, observe that Y e 0 = m 1 X p=1 Y e (q;p) for any 1 q m (7.4) (here we use notation identifying (q; p) = j). Hence Y e 0 2 N m 4 (P m 1 ).

Finally, from (7.4) we have Y (e 0 e (q;p) ) = P m 1 s=1; s6 =q Y e (q;s) .

Thus Y 2 M(N m 4 (P m 1 )), and the statement follows.

Linear lower bound on the \Boolean degree" of Positivstellensatz Calculus refutations of the knapsack

We use the following notation from IPS99, Gri01a]. For a polynomial f, its multilinearization f is a polynomial obtained by the reduction of f modulo (x x 2 ) for every variable x, i.e., f is the unique multilinear polynomial equivalent to f modulo these (\Boolean") polynomials. When f = f we say that f is reduced.

For a monomial t one can de ne its Boolean degree Bdeg(t) as deg(t), in other words, the number of occurring variables; then one extends the concept of Bdeg to polynomials: Bdeg(f) = maxBdeg(t i ), where the maximum is taken over all non-zero monomials t i occurring in f. Thereby, one can de ne Bdeg of a derivation in PC and subsequently in Positivstellensatz and Positivstellensatz Calculus as maximum Bdeg of all polynomials in the derivation (in Positivstellensatz and Positivstellensatz Calculus, this includes polynomials h 2 j , cf. de nition in Subsection 2.2).

The following lemma extends the argument in the proof of IPS99, Theorem 5.1] from deg to Bdeg.

Lemma 8.1. Let f(x 1 ; : : : ; x n ) = c 1 x 1 + +c n x n m, where c 1 ; : : : ; c n 2 Rnf0g. Let q be deducible in PC from the knapsack problem f = 0 with Bdeg d(n 1)=2e.

Then one can represent q = n X i=1 (x i x 2 i )g i + fg; (8.1) where deg(fg) Bdeg(q). Proof. Similarly to the proof of IPS99, Theorem 5.1], we conduct the induction along a ( xed) deduction in PC. Assume (8.1) and consider a polynomial qx 1 obtained from q by multiplying it by a variable x 1 . W.l.o.g. one can suppose that g is reduced. Then qx 1 = fgx 1 ; denote h = gx 1 . Let d = deg(h) 1. We need to verify that d + 2 = deg(fh) Bdeg(qx 1 ). Taking into account that d + 1 = deg(h) deg(g) + 1 = deg(fg) Bdeg(q) Bdeg(qx 1 ); the mere case to be brought to a contradiction is when Bdeg(qx 1 ) = Bdeg(q) = deg(g) + 1 = d + 1.

We write g = p + x 1 p 1 where all the terms of g not containing x 1 are gathered in p. Clearly, deg On the other hand, d = Bdeg(q) 1 d(n 1)=2e 1. Therefore, IPS99, Lemma 5.2] applied to the instance c 2 x 2 +: : :+c n x n 0 of symmetric knapsack states that deg((c 2 x 2 + : : : + c n x n )p) = deg(p) + 1 = d + 1 (one should add to the formulation of IPS99, Lemma 5.2] the condition that p is reduced).

Hence there exists a monomial x J = Q j2J x j occurring in p for a certain J f2; : : :; ng, jJj = d, and besides, there exists i 2 2::n] such that the monomial x i x J , being of the degree d + 1, occurs in the polynomial (c 2 x 2 + + c n x n )p, in particular i 6 2 J.

Because of that the monomial T = x i x J x 1 with deg(T) = d + 2 occurs in p 0 = (c 2 x 2 + + c n x n )px 1 : Furthermore, T occurs in fgx 1 = ((c 2 x 2 + + c n x n ) + (c 1 x 1 m))(p + x 1 p 1 )x 1 since after opening the parenthesis in the right-hand side of the latter expression we obtain only p 0 and two subexpressions (c 1 x 1 m)(p + x 1 p 1 )x 1 = (c 1 m)gx 1 and (c 2 x 2 + + c n x n )x 1 p 1 x 1 of Boolean degree at most d + 1 (thereby, any monomial from these subexpressions cannot be equal to the reduced monomial T). Finally, due to the equality qx 1 = fgx 1 , we conclude that Bdeg(qx 1 ) deg(qx 1 ) = deg(fgx 1 ) d + 2; the achieved contradiction proves the induction hypothesis for the case of the rule of the multiplication by a variable (note that the second rule in (2.2) can be replaced by the multiplication by a variable with a multiplicative constant). Now we proceed to the consideration of the rule of taking the sum of two polynomials q and r. By the induction hypothesis we have r = n X i=1 (x i x 2 i )u i + fu; where u is reduced and deg(fu) Bdeg(r). Then making use of (8.1) we get r + q = fv where v = g + u. The inequality deg(v) maxfdeg(g); deg(u)g maxfBdeg(q); Bdeg(r)g 1 d(n 1)=2e 1 dn=2e 1 enables us to apply IPS99, Lemma 5.2] to v, this implies that deg(fv) = deg(v) + 1 = deg(fv). Therefore, Bdeg(r + q) deg(r + q) = deg(fv) = deg(fv).

The next corollary extends IPS99, Theorem 5.1].

Corollary 8.1. Any PC deduction of the knapsack f has Bdeg greater than d(n 1)=2e: Now we can formulate the following theorem extending the theorem of Gri01a] from deg to Bdeg. Denote by a stairs-form function which equals to 2 out of the interval (0; n) and which equals to 2k + 4 on the intervals (k; k + 1) and (n k 1; n k) for all integers 0 k < n=2.

Theorem 8.1. Any Positivstellensatz Calculus refutation of the symmetric knapsack problem f = x 1 + + x n m has Bdeg greater or equal to minf (m); d(n 1)=2e + 1g: Proof. We follow the line of the proof of the theorem Gri01a]. Suppose to the contrary that there is a Positivstellensatz Calculus refutation with Bdeg < d := minf (m); d(n 1)=2e + 1g: First, we apply Lemma 8.1 to the deduction in PC being an ingredient of the deduction in Positivstellensatz Calculus (see de nitions in 2.2). This provides a Positivstellensatz refutation of the form

1 + X j h 2 j = n X i=1 (x i x 2 i )g i + fg; (8.2)
where Bdeg(fg) deg(h 2 j ) < d.

The rest of the proof follows the idea from Gri01a] of applying the linear mapping B to both sides of (8.2), where B is de ned on the monomials x I as B : R x 1 ; : : : ; It is worthwhile to mention that B is de ned on the quotient algebra R x 1 ; : : : ; x n ]=(x 1 x 2 1 ; : : :; x n x 2 n ), thereby, the proof in Gri01a] actually estimates Bdeg rather than just deg.

We would like to sketch here a streamlined version of the latter proof, invoking at some point technique from the theory of association schemes, cf. e.g. BI84].

Lemma 8.2. (cf. Gri01a, Lemma 1.3].) Let g 0 2 R x 1 ; : : : ; x n ], and Bdeg(g 0 ) < n. Then B(fg 0 ) = 0. Proof. Verify that B(fX I ) = 0 on all the monomials X I of g 0 , as B satis es the recurrence (n k)B k+1 = (m k)B k .

Introduce on (the coe cient space of) R x 1 ; : : : ; x n ]=(x 1 x 2 1 ; : : :; x n x 2 n ) a quadratic form Q by setting Q(x I ; x J ) = B(x I J ) and denote by Q `the restriction of Q onto the subspace of polynomials of degree at most `. In the sequel we allow ourselves to denote by Q `also the matrix of Q `. It is interesting to mention that Q is known as the moment matrix of B, see e.g. Las01, Lau01]. The \if" part of the following statement is Gri01a, Lemma 1.4]. The \only if" part demonstrates that at least along these lines the bound of Theorem 8.1 cannot be improved. Lemma 8.3. (cf. Gri01a, Lemma 1.4].) The form Q `is positive semide nite if and only if ` 1 < m < n `+ 1 and ` bn=2c.

A proof for this lemma is given below, and this is where the promised streamlining happens. We now demonstrate how to deduce the proof of the theorem from this lemma.

Apply B to the both sides of (8.2). The right-hand side vanishes, as B(fg) = 0 due to Lemma 8.2, and as B((x i x 2 i )g i ) = B(x i g i ) B(x 2 i g i ) = 0. The lefthand side then evaluates to C = 1 + P j h T j Qh j , where h j stands for the vector of coe cients of the polynomials h j . As the maximal degree of h 2 j cannot be larger than the maximal degree of the right-hand side of (8.2), h T j Qh j = h T j Q `hj , where `falls into the range covered by Lemma 8.3. Hence h T j Qh j 0 and thus C > 0, the desired contradiction.

Proof of Lemma 8.3. Let us order the subsets of f1; : : :; ng with respect to the size (i.e. degree), and in arbitrary (but xed) way within each size, and x the ordering on the rows and columns of Q `accordingly. Denote by Q ``the principal submatrix of Q `corresponding to the `-element subsets of f1; : : :; ng (so that Q ``occupies the south-east corner of Q `).

We show now that Q `has at least T n ` zero eigenvalues, where T = P `j=0 n j . To this end, let us exhibit a basis for a subspace of such a dimension of the nullspace ker Q `of Q `. The coe cient vectors of fx I , lie in ker Q `as long as jIj < `, as can be seen by invoking Lemma 8.2 on B(fx I x J ), where jJj `. These fx I will form the desired basis, as these vectors are linearly independent. This can be seen by building a basis for the subspace they generate, adding rst the vector of coe cients of fx I , where I is the greatest (w.r.t. the ordering speci ed above) subset of size jIj < `, then the second greatest I, and so on. At each step a new, smaller, monomial of the form Dx I for D 2 R f0g appears in fx I , implying that the dimension increases, and we are done.

To this point we followed Gri01a] quite closely. Now comes the rst shortcut. Namely, we claim that positive de niteness of Q ``implies positive semide niteness of Q `. Indeed, let 1 ( n `) (resp. 1 T ) be the sequence of the eigenvalues of Q ``(resp., of Q `). It is well-known (the result attributed to Cauchy, and as such sometimes referred to as Cauchy interlacing, as well as the inclusion principle for eigenvalues) that the rst sequence interlaces the second, that is, i i for 1 i n ` , cf. e.g. HJ90, Theorem 4.3.15] or L ut96, 5.3.1(11)]. Therefore the rst n ` eigenvalues of Q `are not smaller than the smallest eigenvalue of Q ``, and thus positive, and we are done.

Already at this point we can prove that Q `is positive semide nite for m suciently close to `, as for m = `the matrix Q ``is a positive scalar multiple of the identity matrix, and as the eigenvalues of Q ``depend continuously on m. (And actually, even for m su ciently close to ` i, for 0 i `, as Q ` i is a principal submatrix of Q `.)

To complete the proof for all the values of m under consideration, we show that Q ``is positive de nite. Here we invoke the theory of association schemes, see e.g. BI84, God93], as follows. For the sake of completeness, we give few de nitions rst. (8.5)

The equality in the second row is obtained by applying to the inner sum in the rst row the procedure described in PWZ96, Chapter 3] that identi es hypergeometric series. Note that the rst non-vanishing term of this sum is the t-th one (i.e. i = t) and it equals ( t) t `t m t . The equality in the third row is derived using the Gauss's identity (see PWZ96, Sect. 3.5]).

Next, we again use the abovementioned procedure from PWZ96, Chapter 3] to identify the latter sum sj B`= P t 0 ft (1+m `)`! as a hypergeometric series. Pulling the constant term 1 (1+m `)`! outside, one notes that the already the 0-th term does not vanish, and equals (1 + m). Thus we just have to compute the ratio of the consecutive summands f t+1 and f t to arrive at f t+1 f t = (t j)(t n + j 1)( t + m `) (m t) (t n + `)(t + 1) (m t + 1) = (t j)(t n + j 1)(t m + `) (t n + `)(t + 1)(t m) ; where the latter is obtained by using the identity (x + 1)= (x) = x. This readily identi es the series and one obtains the following. s j B `

(1 + m `) (1 + m) `! = 3 F 2 m + `; n + j 1; j n + `; m ; 1 = ( n + m) j (` j + 1) j ( n + `)j (m j + 1) j :

Here the Saalsch utz's identity (see PWZ96, Sect. 3.5]) is applied to the second expression for j > 0 to obtain the rightmost expression, that is also valid for j = 0 by de nition of the ascending factorial. We should investigate the sign of R j = ( n+m)j ( n+`)j , as the remaining multiplicative term is positive. Note that the multiplicands of the denominator are always negative. On the other hand, the numerator has all the multiplicands negative if and only if m < n j + 1 for all j. (and in particular R j > 0.) This completes the proof of the \if" part of the lemma.

Arguing along this line it follows that if m > n `+ 1 then there exists j such that one gets R j < 0. Finally, observe that if m < ` 1 then B `< 0. Thus if a condition on m in the lemma is not satis ed then Q ``has a negative eigenvalue. This implies that Q `is not positive semide nite, completing the proof of Lemma 8.3, and, thereby, of Theorem 8.1. 9. Exponential lower bound on the size of static LS + and Positivstellensatz Calculus refutations of the symmetric knapsack

In this section we apply the results of Section 8 to obtain an exponential lower bound on the size of static LS + and Positivstellensatz Calculus refutations of the symmetric knapsack. We follow the notation introduced in Subsection 2.5 and Section 8. The Boolean degree of a static LS (LS + ) refutation is the maximum Boolean degree of the polynomials u i;l in Subsection 2.5.

Let us x for the time being a certain (threshold) d.

Lemma 9.1. Denote by M the number of monomials of Boolean degrees at least d that occur in a Positivstellensatz Calculus refutation of system of inequalities S. Then there is a variable x such that the result of substituting x = 0 in this refutation is a valid Positivstellensatz Calculus refutation of the system Sj x=0 and contains at most M(1 d=n) (non-zero) monomials of Boolean degrees at least d.

Proof. Since the refutation contains at least M monomials of Boolean degrees at least d, there is a variable x occurring in at least Md=n of these monomials. Therefore, at least Md=n monomials vanish after the substitution.

Lemma 9.2. Denote by M the number of u i;l 's occurring in (2.17) that have Boolean degrees at least d. Then there is a variable x and a value a 2 f0; 1g such that the result of substituting in (2.17) x = a contains at most M(1 d=(2n)) non-zero polynomials u i;l j x=a of Boolean degrees at least d. (Note that by substituting in (2.17) a value a for x we obtain a valid static LS + refutation of the system Sj x=a ).

Proof. Since there are at least Md occurrences of x i or 1 x i in the polynomials u i;l of Boolean degrees at least d, there is a variable x such that either x or 1 x occurs in at least Md=(2n) of these polynomials. Therefore, after substituting the appropriate value for x, at least Md=(2n) polynomials u i;l vanish from (2.17).

For the symmetric knapsack problem (5.2), we can rewrite its static LS + refutation in the following way. Denote f 0 = x 1 + + x n m; f i = x i x 2 i (1 i n); f i = (s 0 i ) 2 (n + 1 i n 0 ) (m is not an integer). The refutation can be represented in the form for appropriate multisets G i;l , G + i;l , T j and T + j , positive real j and arbitrary real i;l . Lemma 9.3. If n=4 < m < 3n=4, then the Boolean degree D of any static LS + refutation of the symmetric knapsack problem is at least n=4.

  Lemma 5.1. Let Y = P n i=1 a i x i , f d (Y ) = (Y (d 1))(Y d), a i are integers, x i are variables. Then the inequality f d (Y ) 0 has a derivation of size polynomial in d, n and max i ja i j in the following systems:

  (p) deg(g) = d. Moreover, deg(p) = d because if deg(p) < d, we would have d + 1 = deg(h) Bdeg(gx 1 ) max(Bdeg(x 1 p); Bdeg(x 2 1 p 1 )) d.

  x n ] ! R; where B(x I ) = B k on the rest of R x 1 ; : : : ; x n ].

  Figure 1. Known simulations between semi-algebraic and other proof systems for formulas in k-DNF. R denotes resolution, CP p denotes CP with polynomially bounded coe cients, NS + denotes Positivstellensatz, PC + denotes Positivstellensatz Calculus, sLS

	sLS 1 + " sLS + " sLS 1 " sLS	LS 1 + " -PC + LS 1 " -" -% " LS+CP 1 NS + PC LS CP LS ;split ; LS 3 = -" " " % NS R ! CP p
	LS LS+CP 2 6 #	LS 4 6 & 6 .	LS d 6 . 6 &

: : : denotes static LS : : : . The simulations between static LS : : : and other proof systems are not shown because static LS : : : are not well-de ned proof systems (see Remark 2.7). Some of the trivial simulations (e.g., the simulation of LS d by LS d : : : ) are not shown for readability. The simulation of CP p is shown in Theorem 5.2. The simulation of PC (resp., PC + ) in LS 1 (resp., LS 1 + ) is shown in Corollary 3.1 (resp., 3.2). R CP PC F c Figure 2. Known separations between semi-algebraic and other proof systems for formulas in DNF (except for PC which is considered for formulas in k-DNF only, i.e., PHP is not a valid counterexample for it): A 6 ! B means that there is a formula that has polynomial-size A proofs and has no polynomial-size B proofs. F c denotes constant-depth Frege systems. See Fig. 1 for other notation. Only the strongest separations relevant to semi-algebraic systems are shown. The leftmost separation is due to PHP (the positive part is proved in Pud99], the negative part is proved in Hak85]

If one can decide in polynomial time for x

L 1 , whether x 2 L, then any proof system for L 1 can be restricted to L L 1 by mapping proofs of elements of L 1 n L into any xed element of L. For example, this is the case for L 1 consisting of all tautologies in DNF and L consisting of all tautologies in k-DNF.

Usually, an arbitrary linear combination is allowed, but clearly it can be replaced by two multiplications and one addition.

Acknowledgment

The authors are grateful to Arist Kojevnikov, Akihiro Munemasa, Alexander Razborov and Hans van Maaren for useful discussions.

The second author is partially supported by grant #1 of the 6th RAS contest-expertiseof young scientists projects and RFBR project 02-01-00089. The research described in this publication was made possible in part by Award No. RM1-2409-ST-02 of the U.S. Civilian Research & Development Foundation for the Independent States of the Former Soviet Union (CRDF). The third author is partially supported by the DFG Grant SCHN-503/2-1. 1 DIMA GRIGORIEV, EDWARD A. HIRSCH, AND DMITRII V. PASECHNIK 4.

We denote by M = M ( n `) (C ) the algebra of the n ` n ` matrices with entries in the eld C of complex numbers. The centralizer C M (S) of an S M in M is de ned by C M (S) = fc 2 M j cs = sc for any s 2 Sg. Note that C M (S) is a subalgebra of M.

Let M be the permutation representation of the symmetric group S n acting on the subsets of size `. That is, one takes each 2 S n as a permutation 0 in S ( n `) by setting 0 (ft 1 ; : : :; t `g) = f (t 1 ); : : :; (t `)g and then turning 0 into a 0-1 matrix ( ) by setting I; 0 (I) ( ) = 1 and IJ ( ) = 0 for the remaining pairs of indices (IJ), J 6 = 0 (I). Then Q ``2 C M ( ). The algebra C M ( ) is known under many di erent names, cf. BI84], e.g. as the Bose-Mesner algebra of the Johnson scheme J(n; `). What is important here is that C M ( ) is commutative of dimension `+ 1, and the 0 1 matrices A i de ned as (A i ) IJ = 1 i jI Jj = i form its basis, 0 i `. As the C -linear representations of nite groups are completely reducible, see e.g. BI84, Theorem 1.2.4], there exists an orthogonal linear transformation that decomposes into a direct sum of `+ 1 irreducible representations. By the Schur's Lemma, see e.g. BI84, Theorem 1.3.2], such a transformation simultaneously diagonalizes all the A i 's, and the restriction of any of the transformed A i 's onto the j-th irreducible constituent is a scalar matrix p i (j)I. Thus each A i has at most `+ 1 distinct eigenvalues p i (j). This implies in particular that, as Q ``= P `i=0 B `+i A i (here B is as in (8.3)), the set of eigenvalues of Q ``equals the set of eigenvalues of (`+ 1) (`+ 1) diagonal matrix P `i=0 B `+i diag(p i (0); p i (1); : : :; p i (`)). To summarize, we state the following lemma, writing out the expressions for p i (j) from BI84, Corollary to Th. 3.2.9].

Lemma 8.4. The set of eigenvalues of Q ``is given by s j = X i=0 B `+i p i (j); where p i (j) = `i n ì 3 F 2 i; j; n 1 + j `; n + `; 1 : (8.4) Here r F s a 1 ; : : :; a r b 1 ; : : :; b s ; y = P t 0 (a1)t:::(ar)t (b1)t:::(as)t y t t! denotes the hypergeometric series and (a) t the ascending factorial (a) t = a(a + 1) : : :(a + t 1), (a) 0 = 1.

To complete the proof of Lemma 8.3, it su ces to show that s j > 0 for all j. Taking (8.3) and (8.4) into account, we see that it remains to show that s j B `= X i 0 `i m ì 3 F 2 i; j; n 1 + j `; n + `; 1 > 0 for 0 j ` Proof. Replacing in t j each occurrence of x i by f i +x 2 i and each occurrence of 1 x i by f i + (1 x i ) 2 and subsequently opening the parentheses in t j , one can gather all the terms containing at least one of f i and separately the products of squares of the form x 2 i , (1 x i ) 2 . As a result one gets a representation of the form n X i=0 f i g i + n 000 X j=1 h 2 j = 1 for appropriate polynomials g i ; h j of Boolean degrees Bdeg(g i ); Bdeg(h 2 j ) D, thereby a Positivstellensatz (and Positivstellensatz Calculus) refutation of the symmetric knapsack of Boolean degree at most D + 2. Then Theorem 8.1 implies that D d(n 1)=2e 1 n=4. Theorem 9.1. For m = (2n + 1)=4 the number of monomials in any Positivstellensatz Calculus refutation of (5.2) is exp( (n)) (hence, the size of such refutation is exponential).

Proof. Now we set d = dn=8e and apply Lemma 9.1 consecutively = bn=4c times.

The result of all these substitutions contains n variables. We denote by f 0 0 the result of the substitutions applied to f 0 (where f 0 = x 1 + + x n m). Note that f 0 0 is again an instance of the knapsack problem. Therefore, we are able to apply Theorem 8.1 to our refutation of f 0 0 . Taking into account that the free term f 0 0 is the same as in f and falls into the interval ((n )=4; 3(n )=4), the degree of this new refutation is at least (n )=4 > d.

Denote by M 0 the number of monomials of the degrees at least d in the original refutation. By Lemma 9.1 the new refutation contains at most M 0 (1 d=n) M 0 (1 1=8) n=4 non-zero monomials of degrees at least d. Since this new refutation contains at least one monomial of such degree, we have M 0 (1 1=8) n=4 1, i.e. M 0 (8=7) n=4 , which proves the theorem. Theorem 9.2. For m = (2n+1)=4 the number of g i;l 's and t j 's in (9.1) is exp( (n)).

Hence, any static LS + refutation of (5.2) for m = (2n + 1)=4 must have size exp( (n)).

Proof. Now we set d = dn=8e and apply Lemma 9.2 consecutively = bn=4c times.

The result of all these substitutions in (9.1) we denote by (9:1 0 ), it contains n variables; denote by u 0 i;l the polynomial we thus get from u i;l . We denote by f 0 0 the result of substitutions applied to f 0 . Note that after all substitutions we obtain again an instance of the knapsack problem. Taking into account that the free term m 0 of f 0 0 ranges in the interval m ; m] and since (n )=4 < m < m < 3(n )=4, we are able to apply Lemma 9.3 to (9:1 0 ). Thus, the degree of (9:

Denote by M 0 the number of u i;l 's of the degrees at least d in (9.1). By Lemma9.2 the refutation (9:1 0 ) contains at most M 0 (1 d=(2n)) M 0 (1 1=16) n=4 non-zero polynomials u 0 i;l of degrees at least d. Since there is at least one polynomial u 0 i;l of such degree, we have M 0 (1 1=16) n=4 1, i.e. M 0 (16=15) n=4 , which proves the theorem.

Corollary 9.1. Any tree-like LS + (or LS 1 ) refutation of (5.2) for m = (2n+1)=4 must have size exp( (n)).

Proof. The size of such tree-like refutation (even the numer of instances of axioms f i used in the refutation) is at least the number of polynomials u i;l .

Remark 9.1. The value m = (2n+1)=4 in Theorems 9.1 and 9.2 and Corollary 9.1 can be changed to any non-integer value between dn=4e and b3n=4c by tuning the constants in the proofs (and in the (n) in the exponent). 10. Open Questions 1. What is the proof complexity of the symmetric knapsack problem in (daglike dynamic) LS (cf. Sections 5, 7 and 9)? We conjecture it (or the general knapsack problem) as a candidate for a lower bound. 2. Prove an exponential lower bound for a static semi-algebraic propositional proof system. Note that we have only proved an exponential lower bound for static LS + as a proof system for the co-NP-complete language of systems of 0-1 linear inequalities, because the symmetric knapsack problem is not obtained as a translation of a Boolean formula in DNF. 3. Suggest a candidate for a lower bound in LS d for (arbitrarily large) constant d. 4. How precise is the logarithmic lower bound on the LS -rank for the knapsack problem from Subsection 7.2? 5. Can one relax in Theorem 5.2 the condition on the polynomial growth of the coe cients? 6. Is it possible to simulate LS (or static LS 1 ) by means of a suitable version of CP (e.g. by the R(CP) introduced in Kra98])? In other words, does there exist an inverse to Theorem 5.2?