Linear Lower Bound on Degrees of Positivstellensatz Calculus Proofs for the

Parity

Dima Grigoriev^{∗}

Abstract It is established a linear (thereby, sharp) lower bound on degrees of Positivstellensatz calculus refutations over a real field introduced in [GV99], for the Tseitin tautologies and for the parity (the mod 2 principle). We use the machinery of the Laurent proofs developped for binomial systems in [BuGI 98], [BuGI 99].

keywords: Positivstellensatz calculus proofs, boolean binomial system, Tseitin tautologies

Introduction

In recent years there was an intensive activity in the research of algebraic proof systems ([BIK 96], [BuGI 98], [BuGI 99], [BuIK 96], [CEI 96], [G 98], [IPS 97]). The approach relies on the Hilbert’s Nullstellensatz and treats the problem of feasibility of a system of polynomial equations

f_{1} = ⋯ = f_{k} = 0,

where among the polynomials f_{1}, …, f_{k} ∈ F [X_{1}, …, X_{n}], there appear the polynomials X_{1}^{2} − X_{1}, …, X_{n}^{2} − X_{n} (so-called, Boolean case). Note that this problem is, in general, NP -complete.

∗IRMAR, Université de Rennes, Campus de Beaulieu, 35042 Rennes, cedex France

The Nullstellensatz proof system (NS) was first considered in [BIK 96]. The aim of the system is to find the polynomials g_{1}, …, g_{k} ∈ F [X_{1}, …, X_{n}] such that 1 = g_{1}f_{1} +⋯+g_{k}f_{k}. The latter representation is sometimes called a Nullstellensatz refutation. The number max_{1≤i≤k}{deg(g_{i}f_{i})} is called the Nullstellensatz degree. A linear upper bound O(n) on the Nullstellensatz degree is evident, in [BIK 96] a non-constant lower bound was proved, while in [G 98] a linear (and thus sharp) lower bound was proved.

In [CEI 96] a stronger proof system — polynomial calculus (PC) was introduced. Starting from axioms f_{1}, …, f_{k}, PC allows to derive from the already obtained polynomials a, b ∈ F [X_{1}, …, X_{n}] more polynomials, according to the following two rules:

1. (additive) a, b ⊢ αa + βb, where α, β ∈ F;

2. (multiplicative) a ⊢ X_{i}a for 1 ≤ i ≤ n.

The aim of a derivation is to reach 1.

The degree of a PC derivation is defined as the maximum of the degrees of all intermediately derived polynomials. The first lower bound on the degrees of PC derivations was obtained in [R 96] (see also [IPS 97] and [BuIK 96]). A linear lower bound for PC was proved in [BuGI 99]. Note that the latter bound is sharp.

In [GV 99] inequalities were involved along with equations into proof systems, in particular we assume that the input polynomials f_{1}, …, f_{k} belong to R[X_{1}, …, X_{n}]. The case of linear inequalities with added conditions X_{i}^{2} = X_{i} (Boolean programming) was widely studied by means of cutting planes proofs, for which an exponential lower bound on the length was obtained (a survey and references can be found in [P 98]). Another approach to systems of linear inequalities was undertaken in [LS 91], [L 94], [ST 98], where a derivation system was introduced which allows from any linear polynomial e, already derived linear inequalities a_{1} ≥ 0, a_{2} ≥ 0 and quadratic inequalities p_{1} ≥ 0, p_{2} ≥ 0, to derive quadratic inequalities e^{2} ≥ 0, a_{1} + a_{2} ≥ 0, a_{1}a_{2} ≥ 0, p_{1} + p_{2} ≥ 0. In [P 98] one can find some remarks on the complexity of this Lovász-Schrijver procedure, in particular, an upper bound for the Pigeon Hole Principle which demonstrates an exponential gap between the complexity of cutting planes proofs and the Lovász-Schrijver procedure.

More precisely, following [GV 99], let a system of equations and inequalities

f_{1} = ⋯ f_{k} = 0, h_{1} ≥ 0, …, h_{m} ≥ 0.  (1)

be given. Dealing with systems of inequalities one could get profit from using the axiom that any square is non-negative, and the rules of adding or multiplying inequalities. This is formalized in the following notion of the cone (which replaces the role of ideals for systems of equations) and in two proof systems described below for refuting systems of inequalities, they extend the systems NS and PC, respectively.

Definition 1 The cone c(h_{1}, …, h_{m}) generated by polynomials h_{1}, …, h_{m} ∈ R[X_{1}, …, X_{n}] is the smallest family of polynomials containing h_{1}, …, h_{m} and satisfying the following rules:

(a) e^{2} ∈ c(h_{1}, …, h_{m}) for any e ∈ R[X_{1}, …, X_{n}];

if a, b ∈ c(h_{1}, …, h_{m}), then

(b) a + b ∈ c(h_{1}, …, h_{m});

(c) ab ∈ c(h_{1}, …, h_{m}).

Remark 1 The minimal cone c(∅) consists of all sums of squares of polynomials.

Remark 2 Any element of c(h_{1}, …, h_{m}) can be represented in a form

∑_{I⊂{1,...,m}}(∏_{i∈I} h_{i})(∑_{j} e_{I,j}^{2})

for some polynomials e_{I,j} ∈ R[X_{1}, …, X_{n}].

Two proof systems (which could be viewed as static and dynamic, respectively) introduced in [GV 99] rely on the following Positivestellensatz (see [BCR 87], [S 74]). Positivstellensatz. A system (1) has no common solutions in R^{n} if and only if for a suitable polynomial f ∈ R[X_{1}, …, X_{n}] from the ideal (f_{1}, …, f_{k}) and a polynomial h ∈ c(h_{1}, …, h_{m}) we have: f + h = −1.

The first (static) proof system is stronger than NS refutations and could be viewed as its Positivstellensatz analogue.

Definition 2 A pair of polynomials

(f, h) = ( ∑_{1≤s≤k} f_{s}g_{s}, ∑_{I⊂{1,...,m}}(∏_{i∈I} h_{i})(∑_{j} e_{I,j}^{2}))

with f + h = −1 where g_{i}, e_{I,j} ∈ R[X_{1}, …, X_{n}] we call a Positivstellensatz refutation (denote it by P S >) for (1). The degree of the refutation is

max_{s,I,j}{deg(f_{s}g_{s}), deg(e_{I,j}^{2} ∏_{i∈I} h_{i})}.

The second (dynamic) proof system is stronger than PC and could be viewed as its Positivstellensatz analogue.

Definition 3 Let a polynomial f ∈ (f_{1}, …, f_{k}) be derived in PC from the axioms f_{1}, …, f_{k}, and a polynomial h ∈ c(h_{1}, …, h_{m}) be derived, applying the rules (a), (b), (c) (see Definition 1), from the axioms h_{1}, …, h_{m}. Suppose that f +h = −1. This pair of derivations we call a Positivstellensatz calculus refutation (denote it by P C >) for (1). By its degree we mean the maximum of the degrees of intermediate polynomials from both derivations. The length of the refutation we define as the total number of steps in both derivations.

In the present paper we consider just the systems of equations f_{1} = ⋯ = f_{n} = 0 (the polynomials h_{1}, …, h_{m} are absent). In this case a polynomial h is just a sum of squares ∑_{j} h_{j}^{2} (cf. remark 1).

In [GV 99] a so-called telescopic system of equations due to Lazard-Mora-Philippon (see [Br 87]) is considered and an exponential lower bound on the degree of any its P S > refutation (see definition 2) is proved. On the other hand it is shown a linear upper bound for the telescopic system on the degree of PC, being sharp because a linear lower bound is proved in [GV 99] for the stronger system of the P C > refutations (see definition 3), and for the latter one also an exponential lower bound on the lengths of proofs is established.

However, the telescopic system is not Boolean, whereas the main interest in the proof theory is just in the Boolean systems. In the present paper we prove a linear lower bound on the degree of P C > refutations for the Tseitin tautologies (see Corollary 1 in section 3) and for the parity (see Corollary 2 in section 3), the proofs extend the argument from [BuGI 98], [BuGI 99]. They follow from the theorem in section 2 in which a lower bound on the degree of the P C > refutations is established for Boolean binomial systems in terms of the Laurent proofs (see [BuGI 98], [BuGI 99] and also section 1 below). Let us mention that unlike the results of [BuGI 98], [BuGI 99] being valid over an arbitrary field F, the results of the present paper involving inequalities, make sense just over real fields.

1 Laurent proofs for Boolean Thue systems

Let F be a field.

A product of variables m = X_{1}^{i_{1}} ⋯ X_{n}^{i_{n}} is called a monomial, and am is called a term where a coefficient a ∈ F^{∗} = F − {0}.

Definition 4 (cf. [G 98], [BuGI 98], [BuGI 99]). A Boolean (multiplicative) Thue system over F in variables X_{1}, …, X_{n} is a family T = {(a_{1}m_{1}, a_{2}m_{2})} of pairs of terms such that (X_{i}^{2}, 1) ∈ T for any 1 ≤ i ≤ n.

Throughout first two sections we fix a Boolean Thue system T.

As in [BuGI 98], [BuGI 99] we consider Laurent monomials l = X_{1}^{i_{1}} ⋯ X_{n}^{i_{n}} with (possibly negative) integer exponents i_{1}, …, i_{n}. A product al where a ∈ F^{∗} is called a Laurent term. Laurent terms constitute a multiplicative group L. We define the degree deg(l) = max{∑_{i_{j}>0} i_{j}, − ∑_{i_{j}<0} i_{j}}.

Definition 5 (cf. [BuGI 98], [BuGI 99]). For any natural number d we construct recursively a subset L_{d} ⊂ L of the terms of degrees at most d. As a base we include in L_{d} any term a_{1}a_{2}^{−1}m_{1}m_{2}^{−1} from T (see definition 4), provided that its degree does not exceed d. As a recursive step for two Laurent terms l_{1}, l_{2} ∈ L_{d} we adjoin the product l_{1}l_{2} in L_{d} if deg(l_{1}l_{2}) ≤ d. Along with each l_{1} ∈ L_{d} we include l_{1}^{−1} ∈ L_{d}. Keep doing the recursion while augmenting L_{d}.

Definition 6 (cf. [BuGI 98], [BuGI 99]). Two terms t_{1}, t_{2} are d-equivalent if t_{1} = lt_{2} for a certain l ∈ L_{d}.

Lemma 1 (cf. [BuGI 98], [BuGI 99]). (i) If t_{1} is d-equivalent to t_{2} then t_{1}X_{j} is d-equivalent to t_{2}X_{j}, 1 ≤ j ≤ n.

(ii) d-equivalence is a relation of equivalence on any subset of the set of all the terms of degrees at most d.

Definition 7 (cf. [BuGI 98], [BuGI 99]). The refutation degree D = D(T) is the minimal d such that L_{d} contains some 1 ≠ a ∈ F^{∗}.

By a support of a class of d-equivalence of terms we mean the set of their monomials. The following lemma comprises few properties of classes of d-equivalence of all the terms of degrees at most d.

Lemma 2 (cf. [BuGI 98], [BuGI 99]). Let d < D. The supports of two classes of d-equivalence either coincide or disjoint. Two classes with the same support are obtained from one another by simultaneous multiplication of all the terms by an appropriate factor b ∈ F^{∗}. Thus, any class could be represented by a vector {c_{m}}_{m} where c_{m} ∈ F^{∗} and m runs over the support. Moreover, two classes with the same support has collinear corresponding vectors.

As usual (cf. [G 98], [BuGI 98], [BuGI 99]) to each Thue system T one can attach a binomial ideal P_{T} ⊂ F [X_{1}, …, X_{n}] generated by the binomials a_{1}m_{1} − a_{2}m_{2} (see definition 4).

Lemma 3 (cf. [BuGI 98], [BuGI 99]). Let d < D. Assume that one can express a certain f ∈ F [X_{1}, …, X_{n}] as a F -linear combination of binomials t_{1} − t_{2} where t_{1} = b_{1}m_{3}, t_{2} = b_{2}m_{4} are d-equivalent and deg(t_{1}), deg(t_{2}) ≤ d. Then such a linear combination could be chosen in a way that both monomials m_{3}, m_{4} occur in f (this holds for all occurring binomials t_{1} − t_{2}).

Proof. Take any term am occurring in f. The vector of coefficients of a binomial t_{1} − t_{2} (which has just two nonzero coordinates) is orthogonal to the vector {1/c_{m}}_{m} for the support of every class of d-equivalence (see lemma 2). Hence the vector of the coefficients of f is also orthogonal to the vector {1/c_{m}}_{m}. Therefore, there exists another term a_{0}m_{0} occurring in f with m_{0} from the support of the same class of d-equivalence as am. Due to lemma 2 am is d-equivalent to a suitable term a0^{′}m_{0}. Then the polynomial f − (am − a0^{′}m_{0}) has less terms than f does, and we complete the proof of the lemma by induction on the number of terms in a polynomial. □

Lemma 4 (cf. [BuGI 98], [BuGI 99]). If a polynomial f is deduced from P_{T} in the fragment of the polynomial calculus of a degree at most d < D then f can be expressed as a suitable F -linear combination of binomials of the form t_{1}−t_{2} for d-equivalent t_{1} = b_{1}m_{3}, t_{2} = b_{2}m_{4} where deg(t_{1}), deg(t_{2}) ≤ d. Moreover, such a linear combination could be chosen in a way that both monomials m_{3}, m_{4} occur in f for any binomial t_{1} − t_{2} from the linear combination.

The proof of the lemma proceeds by a direct induction along the inference of f in the PC. Herein after each inference step g_{1}, g_{2} → g_{1} + g_{2} we apply lemma 3. For justifying any inference step g_{1} → aX_{i}g_{1} we apply lemma 1(i). □

The previous lemmas are valid for an arbitrary (not necessary Boolean) Thue system (see [BuGI 98], [BuGI 99]), from now on we take into the account that T is just a Boolean Thue system.

Lemma 5 Let d < D/2 and a Laurent term al ∈ L_{d}. Then a ∈ {−1, +1}.

Proof. Since al ∈ L_{d} ⊂ L_{D−1} we obtain (al)^{2} ∈ L_{D−1} because deg(l^{2}) < D. Let l = X_{1}^{i_{1}} ⋯ X_{n}^{i_{n}}. Taking into the account that X_{1}^{2}, …, X_{n}^{2} ∈ L_{D−1}, we conclude that l^{2} ∈ L_{D−1}, hence a^{2} ∈ L_{D−1}, i.e. a^{2} = 1 by definition 7. □

2 Positivstellensatz calculus proofs for Boolean binomial systems

The results of the previous section are valid for an arbitrary field F (actually, over a commutative ring, with some modifications [BuGI 98], [BuGI 99]). In the sequel we suppose that F is a real field [BCR 87] (in particular, −1 cannot be represented as a sum of squares).

Assume now that we are given a P C > refutation (see definition 3 and the remark after it) of a Boolean binomial ideal P_{T} (taking into account remark 1 from the introduction):

1 + ∑_{j} h_{j}^{2} = ∑_{i} f_{i}g_{i}  (2)

where the binomials f_{i} = a_{1}m_{1} − a_{2}m_{2} ∈ P_{T} (cf. definition 4).

The main purpose of this section is to prove the following lower bound on the degree of the P C > refutations.

Theorem. The degree of any P C > refutation of a Boolean binomial ideal P_{T} (over a real field) is greater or equal to D/2.

Suppose that the right-hand side ∑_{i} f_{i}g_{i} of (2) is deduced in the PC within a degree d_{0} < D/2. Therefore, d_{0} is an upper bound on the degree of P C > refutations of P_{T} since deg(h_{j}^{2}) ≤ deg(∑_{i} f_{i}g_{i}) (to show the latter inequality consider the highest with respect to the deglex monomial ordering term from all the polynomials h_{j}, then the coefficient at the square of this monomial in the sum 1 + ∑ h_{j}^{2} should be positive).

Due to lemma 4 one can represent

∑_{i} f_{i}g_{i} = ∑(b_{1}m_{3} − b_{2}m_{4})  (3)

where in each summand from the right-hand side the terms b_{1}m_{3} and b_{2}m_{4} are d_{0}-equivalent and occur in the left-hand side ∑_{i} f_{i}g_{i}, in particular, deg(m_{3}), deg(m_{4}) ≤ d_{0}.

We introduce the following linear mapping ϕ from the space of polynomials of the degree at most d_{0} to F. It suffices to define ϕ for all the monomials of the degree at most d_{0}. If a monomial is d_{0}-equivalent to a certain element b ∈ F^{∗} then ϕ sends this monomial to b, otherwise ϕ sends the monomial to zero. The mapping ϕ is correctly defined because b is unique, provided it does exist, due to lemma 1(ii) and to definition 7. Now let us consider the result of application of ϕ to the polynomial ∑_{i} f_{i}g_{i}. It can be calculated in two different ways: denote by Σ_{(2)} the result of the evaluation of ϕ at the polynomial 1 + ∑_{j} h_{j}^{2} and by Σ_{(3)} the result of evaluation of ϕ at the polynomial ∑(b_{1}m_{3} − b_{2}m_{4}). Evidently, Σ_{(2)} = Σ_{(3)}. If b_{1}m_{3} is d_{0}-equivalent to a certain b ∈ F^{∗} (see (3)) then b_{2}m_{4} is also d_{0}-equivalent to b (again due to lemma 1(ii)). Therefore, Σ_{(3)} = 0.

On the other hand, we will prove the following

Lemma 6 Σ_{(2)} ≥ 1

which would lead to a contradiction with the supposition d_{0} < D/2 and complete the proof of the theorem. Proof of lemma 6. Fix for a time being one of the items h = h_{j} = ∑_{I} a_{I}X^{I} (see (2)) where the latter sum contains q terms of the form a_{I}X^{I}, a_{I} ∈ F^{∗}, I ∈ Z^{n} being a multiindex. Then deg(X^{I}) ≤ (1/2)deg(∑ f_{i}g_{i}); indeed, to show the latter again as above consider the highest (with respect to the deglex monomial ordering) term in all polynomials h_{j}, see (2). Hence deg(X^{I}) ≤ d_{0}/2 < D/4.

Introduce an (undirected) graph Q with q vertices which correspond to the monomials X^{I} occurring in h (we identify a vertex with the corresponding I). The graph Q contains an edge (I, J) if and only if bX^{I}X^{J} ∈ L_{d_{0}} for a pertinent b ∈ F^{∗}. Since (X^{I})^{2} ∈ L_{d_{0}} for any vertex I (cf. the proof of lemma 5), we treat also the loop (I, I) as an edge of Q.

Observe that after opening the parenthesis in the square h^{2} = h_{j}^{2}, just the terms 2a_{I}a_{J}X^{I}X^{J} (in addition to the terms (a_{I}X^{I})^{2}), where (I, J) is an edge of Q not being a loop, give contribution to the sum Σ_{(2)} under consideration.

Let us show that the graph Q is a (disjoint) union of cliques. Indeed, assume that (I, J) and (J, K) are two edges of Q. Then b_{1}X^{I}X^{J}, b_{2}X^{J}X^{K} ∈ L_{d_{0}} for suitable b_{1}, b_{2} ∈ F^{∗}. We have (b_{2}X^{J}X^{K})^{−1} ∈ L_{d_{0}} and b_{1}(b_{2})^{−1}X^{I}(X^{K})^{−1} ∈ L_{d_{0}} (see definition 5), hence b_{1}(b_{2})^{−1}X^{I}X^{K} ∈ L_{d_{0}} because (X^{K})^{2} ∈ L_{d_{0}} and deg(X^{I}X^{K}) ≤ d_{0}. Thus, (I, K) is also an edge of Q.

Fix for a time being a clique C of Q. Our next purpose is to prove that the contribution Σ_{C} of the terms corresponding to the egdes of C into the sum Σ_{(2)} is non-negative. Note that the contribution of the term (a_{I}X^{I})^{2} into Σ_{(2)} equals to a_{I}^{2} since (X^{I})^{2} ∈ L_{d_{0}}. For every edge (I, J) of C either X^{I}X^{J} ∈ L_{d_{0}} holds (in this case we label (I, J) by 1) or −X^{I}X^{J} ∈ L_{d_{0}} holds (in this case we label (I, J) by −1) due to lemma 5. For each triple of vertices I, J, K of C the product of the labels of three edges (I, J), (J, K), (K, I) equals to 1 (see definition 5). Therefore, one can partition the vertices of C into two parts V_{1}, V_{2}: if an edge links two vertices from the same part then it is labeled by 1, otherwise it is labeled by −1. Hence Σ_{C} =

∑_{I∈V_{1}∪V_{2}}(a_{I})^{2} + 2 ∑_{I_{1},J_{1}∈V_{1}} a_{I_{1}}a_{J_{1}} + 2 ∑_{I_{2},J_{2}∈V_{2}} a_{I_{2}}a_{J_{2}} − 2 ∑_{I_{1}∈V_{1},I_{2}∈V_{2}} a_{I_{1}}a_{I_{2}}

= ( ∑_{I_{1}∈V_{1}} a_{I_{1}})^{2} + ( ∑_{I_{2}∈V_{2}} a_{I_{2}})^{2} − 2( ∑_{I_{1}∈V_{1}} a_{I_{1}})( ∑_{I_{2}∈V_{2}} a_{I_{2}}) ≥ 0.

Thus, the contribution into the sum Σ_{(2)} of each h_{j} from the left-hand side of (2) is non-negative. □

3 Lower bounds on Positivstellensatz calculus refutations for the Tseitin tautologies and the parity

The purpose of this section is to prove lower bounds on the degrees of P C > refutations for Tseitin tautologies (see [T 68], [U 95], [G 98], [BuGI 98], [BuGI 99]) and for the parity (or mod 2 principle, see [BuGI 98], [BuGI 99]).

To describe Tseitin tautologies mod 2 (following [BuGI 98], [BuGI 99] we denote them by T S_{k}(2)) we start with an (undirected) graph G. To each its node v a charge u_{v} ∈ {−1, 1} is assigned with the property that ∏_{v} u_{v} = −1. Besides, we assign to each edge e of G a variable X_{e}.

We construct a Boolean Thue system T = T_{G} (see definition 4) according to these data. The system T_{G} contains a pair of terms (for each node v) (X(v) = u_{v} ∏ X_{e}, 1) where the product ranges over all the edges e incident to v (apart from the Boolean pairs (X_{e}^{2}, 1)).

One can obviously deduce in T that ∏_{v} u_{v} = 1 and thereby in the PC the element 1 − ∏_{v} u_{v} ∈ F^{∗} (which actually equals to 2) from the binomial ideal P_{T} (see section 2).

Any Laurent monomial in the variables {X_{e}}_{e} could be reduced using the Boolean pairs to the (uniquely defined) multilinear monomial (we call it reduced). By the pseudo-degree of a monomial we mean the number of variables which occur in its reduction. Observe that the pseudo-degree of a Laurent monomial does not exceed the double degree of this Laurent monomial (see section 1).

From now on we assume that G = G_{k} is an expander [LPS 88], [M 88] with k nodes and being r-regular (r will be a constant, one could take, say r = 6 [LPS 88], [M 88]). That means that for any subset S of the set of the nodes of G the number of adjacent to S nodes in G is at least (1 + ϵ(1 − |S|/k))|S| for an appropriate constant ϵ > 0. The corresponding to G_{k} Boolean Thue system we denote by T S_{k}(2).

Any Laurent monomial in {X_{e}^{2}}_{e}, {X(v)}_{v} could be also (uniquely) reduced invoking the Boolean pairs, to a multilinear monomial in {X(v)}_{v} (obviously, this reduction does not change the pseudo-degree). By a weight of such a Laurent monomial we mean the number of X(v) which occur in the reduced product.

The following lemma is similar to lemma 2 [G 98] (see also [BuGI 98], [BuGI 99]) and its item (i) justifies the correctness of the described reduction and of the weight because ∏_{v} X(v) = −1 ≠ 1.

Lemma 7 (i) Any reduced monomial in {X_{e}^{2}}_{e}, {X(v)}_{v} which is equal to an element of the form am^{2} where a ∈ F^{∗} and m is a monomial, is either 1 or ∏_{v} X(v) = −1;

(ii) For any 1/2 ≥ ϵ_{1} > 0 there exists ϵ_{0} > 0 such that any reduced monomial in {X_{e}^{2}}_{e}, {X(v)}_{v} with the weight between ϵ_{1}k and (1 − ϵ_{1})k has the pseudo-degree at least ϵ_{0}k.

Proof. (i) If not all X(v) occur in the reduced (non-empty) product U then (due to the connectedness of expanders) there is an edge e = (v_{1}, v_{2}) of G such that X(v_{1}) occurs in U and X(v_{2}) does not occur in U. Hence U contains X_{e} with the exponent 1 and thereby, could not be of the form am^{2}.

(ii) Denote by S the set of nodes v of G such that X(v) occurs in U. Then applying to S the property of the expanders, we conclude that there are at least ϵ_{0}k edges of G with one endpoint in S and another endpoint not in S for a suitable ϵ_{0}. These edges give a contribution to the pseudo-degree of U. □

The following lemma is similar to lemma 5.9 [U 95] and to lemma 4 [G 98] (see also [BuGI 98], [BuGI 99]).

Lemma 8 The refutation degree D = D(T S_{k}(2)) is greater than Ω(k).

Proof. By definition 7 there exists a chain of Laurent monomials l_{1}, …, l_{N} in {X_{e}^{2}}_{e}, {X(v)}_{v} such that 1 ≠ l_{N} ∈ F^{∗} and that each l_{j} is either one of {X_{e}^{2}}_{e}, {X(v)}_{v}, either l_{j_{1}}^{−1} or l_{j_{1}}l_{j_{2}} for some j_{1}, j_{2} < j, moreover the degree of each l_{j} does not exceed D. Then the pseudo-degrees of l_{j} do not exceed 2D (see above). Due to lemma 7(i) l_{N} = −1 and the weight w(l_{N}) = k. Since w(X(v)) = 1 and w(l_{j}) ≤ w(l_{j_{1}}) + w(l_{j_{2}}), we conclude that there exists 1 < j_{0} < N for which (1/3)k ≤ w(l_{j_{0}}) ≤ (2/3)k. Then lemma 7(ii) implies that the pseudo-degree of l_{j_{0}} is greater or equal to ϵ_{0}k. □

Lemma 8 and the theorem (see section 2) entail the following linear (thereby, sharp) lower bound on the degree of P C > refutations for the Boolean binomial system corresponding to Tseitin tautologies.

Corollary 1 The degree of any P C > refutation of the Boolean binomial system P_{T S_{k}(2)} is greater than Ω(k).

Following [BuGI 98], [BuGI 99] we consider (the negation of) mod 2 principle (or the parity) as a system of equations in \binom{n}{2} variables X_{e} where e ⊂ {1, …, n}, |e| = 2, denoted by MOD_{2}^{n}:

X_{e}^{2} = X_{e}; X_{e}X_{f} = 0 for every e, f such that e ≠ f, e ∩ f ≠ ∅;

1 = ∑_{i∈e} X_{e} for each i ∈ {1, …, n}.

Obviously, MOD_{2}^{n} is feasible if and only if n is even.

Note that MOD_{2}^{n} is not a binomial system unlike P_{T S_{k}(2)}.

Definition 8 (see [BuGI 98], [BuGI 99]). Let P = P (x_{1}, …, x_{n}), Q = Q(y_{1}, …, y_{m}) be two sets of polynomials. Then P is (d_{1}, d_{2})-reducible to Q if for every 1 ≤ i ≤ m there exists a polynomial s_{i}(x_{1}, …, x_{n}) of a degree at most d_{1} such that there exists a degree d_{2} derivation in the PC of the polynomials Q(s_{1}, …, s_{m}) from the polynomials P.

Lemma 9 (cf. [BuGI 98], [BuGI 99]). Suppose that P is (d_{1}, d_{2})-reducible to Q. Then if there is a degree d_{3} P C > refutation of Q then there is a degree max{d_{2}, d_{3}d_{1}} P C > refutation of P.

Lemma 10 (see [BuGI 98], [BuGI 99]). For all k the Boolean binomial system P_{T S_{k}(2)} is (4r, 4r)-reducible to MOD_{2}^{k(1+2r)} (where r denotes the valency of the expander G_{k}, one could take r = 6, see above).

Lemmas 9, 10 and Corollary 1 imply the following linear (thereby, sharp) lower bound on the degree of P C > refutations for the parity.

Corollary 2 (cf. [BuGI 98], [BuGI 99]). The degree of any P C > refutation of MOD_{2}^{k} is greater than Ω(k).

References

[BIK 96] P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi, and P. Pudlák “Lower bounds on Hilbert’s Nullstellensatz and propositional proofs,” Proc. London Math. Soc., V. 73, 1996, 1–26.

[BCR 87] J. Bochnak, M. Coste, and M.-F.Roy “Real algebraic geometry,” Springer-Verlag, 1998.

[Br 87] D. Brownawell “Bounds for the degrees in the Nullstellensatz,” Ann. Math., 1987, V. 126, 577–591.

[BuGI 98] S. Buss, D. Grigoriev, R. Impagliazzo, and T. Pitassi “Linear gaps between degrees for polynomial calculus modulo distinct primes,” Proc. 31st Ann. ACM Symp. on Theory of Computing, 1999, 547–556.

[BuGI 99] S. Buss, D. Grigoriev, R. Impagliazzo, and T. Pitassi “Linear gaps between degrees for polynomial calculus modulo distinct primes,” To appear in J. Comput. Syst. Sci.

[BuIK 96] S. R. Buss, R. Impagliazzo, J. Krajíček, and P. Pudlák, A. Razborov, and J. Sgall “Proof complexity in algebraic systems and bounded depth Frege systems with modular counting,” Computational Complexity, 6, 1996/1997, 256–298.

[CEI 96] M. Clegg, J. Edmonds, and R. Impagliazzo “Using the Groebner basis algorithm to find proofs of unsatisfiability,” Proc. 28th Ann. ACM Symp. on Theory of Computing, 1996, 174–183.

[G 98] D. Grigoriev “Nullstellensatz lower bounds for Tseitin tautologies,” Proc. 39th Ann. IEEE Symp. on Foundations of Computer Science, 1998, 648–652.

[GV99] D. Grigoriev and N. Vorobjov “Complexity of Null- and Positivstellensatz proofs,” submitted to Ann. Pure Appl. Logic

[IPS 97] R. Impagliazzo, P. Pudlák, and J. Sgall “Lower bounds for polynomial calculus and the Groebner basis algorithm,” Computational Complexity, V. 8, 1999, 127–144.

[L 94] L. Lovász “Stable sets and polynomials,” Discrete Mathematics, V. 124, 1994, 137–153.

[LS 91] L. Lovász and A. Schrijver “Cones of matrices and set-functions and 0–1 optimization,” SIAM J. Optimization, V. 1, 1991, 166–190.

[LPS 88] A. Lubotzky, R. Phillips and P. Sarnak “Ramanujan graphs,” Combinatorica, V. 8, 1988, 261–277.

[M 88] G. Margulis “Explicit group-theoretical construction of combinatorial schemes and their applications to the design of expanders and concentrators,” Problems Inform. Transm., V. 24, 1988, 39–46.

[P 98] P. Pudlák “On the complexity of the propositional calculus,” Preprint, 1998.

[R 96] A. Razborov “Lower bounds for the polynomial calculus,” Computational Complexity, V. 7, 1998, 291–324.

[S 74] G. Stengle “A Nullstellensatz and a Positivstellensatz in semialgebraic geometry,” Math. Ann., V. 207, 1974, 87–97.

[ST 98] T. Stephen and L. Tunçel “On representation of the matching polytope via semidefinite liftings,” Preprint, 1998.

[T 68] G. Tseitin “On the complexity of derivations in propositional calculus,” in: Studies in mathematics and mathematical logic, V. 2, 1968, 115–125.

[U 95] A. Urquhart “The complexity of propositional proofs,” Bull. Symb. Logic, V. 1, 1995, 425–467.