Tseitin’s Tautologies and Lower Bounds for Nullstellensatz Proofs

D. Grigoriev^{1}

Departments of Mathematics and Computer Science

The Pennsylvania State University

University Park, PA 16802 dima@cse.psu.edu

We use the known linear lower bound for Tseitin’s tautologies for establishing linear lower bounds on the degree of Nullstellensatz proofs (in the usual boolean setting) for explicitly constructed systems of polynomials of a constant (in our construction 6) degree. It holds over any field of characteristic distinct from 2. Previously, a linear lower bound was proved [14] for an explicitly constructed system of polynomials of a logarithmic degree.

Introduction.

In the theory of effective Nullstellensatz the double exponential upper bound d^{2^{O(n)}} [15] on the degrees for general ideals and d^{O(n)} [2], [8] for the unit ideal are well known (here d is the degree and n is the number of variables of the input polynomials). These bounds are known to be sharp due to [13] for the first bound and for the second bound due to the example of Lazard-Mora-Philippon (see [2]).

In the proof system theory (see e.g. [3], [7], [6], [4], [14], [10] ) a similar question is studied when among input polynomials f_{1}, …, f_{k} ∈ F [X_{1}, …, X_{n}] necessarily the polynomials X_{i}^{2} − X_{i}, 1 ≤ i ≤ n appear (let us call such a system of input polynomials a boolean system). Then the known methods [13], [5] for obtaining lower bounds on the degrees of g_{1}, …, g_{k} ∈ F [X_{1}, …, X_{n}] such that ∑ f_{i}g_{i} = 1 (the latter representation is called a boolean Nullstellensatz refutation), provided it does exist (i.e. f_{1}, …, f_{k} have no common zero), fail.

Notice that one could assume all g_{i} to be multilinear, in particular, their degrees are at most n. So, the goal is to establish the linear in n lower bounds on the degrees

1Partially supported by NSF Grant CCR-9424358. of g_{1}, …, g_{k}.

In [14] the first such method was designed which allowed to prove linear lower bounds (even for the polynomial calculus, being a more powerful proof system rather than the Nullstellensatz proofs) for a system of polynomials of a logarithmic degree which describes a modification of the into pigeon-hole principle (an exposition of this method see also in [10]). It holds over an arbitrary field. But for many other systems of polynomials the issue of lower bounds still remains open. Let us also mention that in the earlier papers [3], [7], [6], [4] the methods for obtaining somewhat weaker than linear bounds were exhibited.

It seems to be an interesting general question, how to obtain lower bounds for boolean Nullstellensatz refutations. In this paper we develop an approach which allows to produce explicitly a system of polynomials of degree 6 and to prove a linear lower bound on the degree of its boolean Nullstellensatz refutation. This approach borrows an idea from [13] to reduce the issue of Nullstellensatz refutations to Thue systems. First, we introduce and study (see section 1) boolean multiplicative Thue systems (basically, they consist of binomials necessarily containing among them the polynomials X_{i}^{2}−1, 1 ≤ i ≤ n). They extend slightly Tseitin’s tautologies [16], [9], [17], [18]. We exploit the construction of the Tseitin’s tautologies ([9], [17], [18]), based on expanders ([1], [11], [12]) and give a somewhat simpler proof of a linear lower bound for the case of used in section 1 notion of refutations (lemma 4). Relying on it, we first prove a linear lower degree bound for Nullstellensatz refutations for the systems which include the polynomials X_{i}^{2} − 1, 1 ≤ i ≤ n (theorem 1) and thereupon, for the more customary boolean case of the polynomials X_{i}^{2} − X_{i}, 1 ≤ i ≤ n (corollary 1 in section 2).

Some shortcoming is that theorem 1 (and thereby, corollary 1) does not hold over fields of characteristic 2. To get rid of the latter restriction, at the end of section 2 we consider boolean Thue systems relative the polynomials X_{i}^{2} − X_{i}, 1 ≤ i ≤ n. Unfortunately, in this case the best established bound is merely Ω(log n).

In section 3 we consider boolean Nullstellensatz refutations for the Knapsack problem over any infinite field and prove a linear lower bound for it. For zero characteristic fields a similar result for the subset sum problem was shown in [10].

1 Boolean Multiplicative Thue Proof Systems

Let F be a field with characteristic distinct from 2. Definition 1 A boolean multiplicative Thue system over F in variables X_{1}, …, X_{n} is a family T which consists of terms of two types:

X_{i}^{2} for all 1 ≤ i ≤ n  (1)
σX_{1}^{j_{1}} ⋯ X_{n}^{j_{n}}, j_{1}, …, j_{n} ∈ {0, 1} , σ ∈ {−1, 1} (2)

The system T is satisfiable if all the terms from (1),

(2) equal to 1 for certain X_{1}, …, X_{n} (evidently, all X_{1}, …, X_{n} belong to {−1, 1}).

Using (1) repeatedly one can reduce each term σX_{1}^{j_{1}} ⋯ X_{n}^{j_{n}} with integer j_{1}, …, j_{n} to the form (2), throughout this section we consider terms in this reduced form, then the multiplication of monomials X_{1}^{j_{1}} ⋯ X_{n}^{j_{n}} corresponds to the sum of their exponent vectors (j_{1}, ⋯, j_{n}) over GF (2). Definition 2 A refutation for T is a sequence of (reduced) terms m_{0}, …, m_{N} such that m_{i−1}m_{i} is one of the terms from (2) (after the reductions by (1)) for each 1 ≤ i ≤ N and −m_{N} = m_{0} = 1. The degree of the refutation is the maximum of the degrees of m_{1}, …, m_{N}.

Obviously, if there is a refutation then T is not satisfiable. The completeness proof in the next lemma is standard, cf. e.g. lemma 5.3 [18]. Lemma 1 a) If T is not satisfiable then there is a refutation.

b) There is a polynomial-time (moreover, from NC) algorithm for testing satisfiability. Proof Consider the following linear system L_{T} over GF (2) in the variables z_{1}, …, z_{n}. For each term of type (2) include in L_{T} the following linear equation: j_{1}z_{1} + ⋯ + j_{n}z_{n} = χ(σ), where χ(1) = 0, χ(−1) = 1. The system L_{T} is solvable if and only if T is satisfiable. If L_{T} is not solvable then a suitable linear combination (or in other words, the sum of a subset of the set) of its equations gives 0 at the left side and 1 at the right side. Then the product of all the terms corresponding to this subset, provides a refutation. Lemma is proved.

Boolean multiplicative Thue systems extend slightly Tseitin’s tautologies [16], and a refutation could be viewed as a special form of resolutions, we need just this form for the lower degree bound on the Nullstellensatz refutations in the next section. We exploit the construction [9], [17], [18] of the Tseitin’s tautologies, based on expanders with a linear degree lower bound and give for it a somewhat simpler proof for the sake of self-containdness.

Remind (see e.g. [1]) that an expander G_{n} is a bipartite graph with two parts of vertices A = {A_{1}, …, A_{n}}, B = {B_{1}, …, B_{n}}, where |A| = |B| = n such that G_{n} is 6-regular and for some constant c > 0 (the calculations in [11], [1] show that one could take c = (6\sqrt{5} − 5)/18, but we will not use it) any subset D ⊂ A, contains at least (1 + c (1 − \frac{|D|}{n})) |D| adjacent vertices in B (the roles of A and B could be interchanged).

The system T_{n} under producing has 6n variables X_{1}, …, X_{6n}. Every variable among X_{1}, …, X_{6n} we identify with a corresponding edge of G_{n}. To any vertex A_{i} ∈ A, 1 ≤ i ≤ n corresponds the monomial X^{a_{i}} (having the degree 6) from T_{n} (of type (2)), being the product of the edges incident to A_{i}, where a_{i} ∈ (GF (2))^{6n}. Renumerating (if necessary) the variables one can assume that X_{1} is incident to B_{1} ∈ B. Then include in T_{n} the monomials X^{b_{2}}, …, X^{b_{n}} (each of degree 6) similar as above and the monomial X_{1}X^{b_{1}} of degree 5. Finally, add to (2) the term −X_{1}. The obtained system T_{n} is not satisfiable because the product of all its terms of type (2) equals to −1 (obviously, X^{a_{1}} ⋯ X^{a_{n}} = X^{b_{1}} ⋯ X^{b_{n}} = X_{1} ⋯ X_{6n}). Denote X_{1}X^{b_{1}} = X^{b′_{1}}.

For any GF (2)-linear combination α_{1}a_{1} +⋯ α_{n}a_{n} + β_{1}b′_{1}+β_{2}b_{2}+⋯+β_{n}b_{n} ∈ (GF (2))^{6n} we define its degree as the number of ones (thus, the degree of the corresponding monomial (X^{a_{1}})^{α_{1}} ⋯ (X^{a_{n}})^{α_{n}}(X^{b′_{1}})^{β_{1}} ⋯ (X^{b_{n}})^{β_{n}}) and its weight as the number of ones among α_{1}, …, α_{n}, β_{1}, …, β_{n}. Lemma 2 a) The vectors a_{1}, …, a_{n}, b′_{1}, b_{2}, …, b_{n} are linearly independent.

b) For any constant 0 < c_{1} < 1 there exists a constant c_{0} > 0 such that any linear combination with a weight between c_{1}n and (2 − c_{1})n has the degree greater than c_{0}n. Proof a) Let a = α_{1}a_{1} + ⋯ + α_{n}a_{n}, b = β_{1}b′_{1} + β_{2}b_{2} + ⋯ + β_{n}b_{n} and a + b = 0. Observe that the supports of the vectors a_{1}, …, a_{n} are pairwise disjoint, the same is valid for the vectors b′_{1}, b_{2}, …, b_{n}. Hence the weights of the vectors a and b are equal, denote this weight by s. Let α_{γ_{1}} = ⋯ = α_{γ_{s}} = β_{δ_{1}} = ⋯ β_{δ_{s}} = 1. If s = n then a_{1} +⋯+a_{n} +b′_{1} +b_{2} +⋯+b_{n} = (1, 0, …, 0), so one can assume that s < n. Applying the property of expanders to the set {A_{γ_{1}}, …, A_{γ_{s}}} ⊂ A we get a variable X_{j} which occurs in the monomial X^{a_{γ_{1}}} ⋯ X^{a_{γs}} without occurring in X^{b_{δ_{1}}} ⋯ X^{b_{δs}}. Thus, the j-th coordinate of the vector a + b does not vanish.

b) Consider a linear combination a + b. Denote by s the weight of a and by t the weight of b. Let for definiteness s ≥ t and α_{γ_{1}} = ⋯ = α_{γ_{s}} = β_{δ_{1}} = ⋯ = β_{δ_{t}} = 1 (the case t ≥ s is considered in a similar way). Then \frac{c_{1}}{2} n ≤ s. Applying the property of expanders to the set {A_{γ_{1}}, …, A_{γ_{s}}} ⊂ A, we obtain at least c_{0}n = c (1 − \frac{c_{1}}{4} ) \frac{c_{1}}{4} n variables which occur in X^{a_{γ_{1}}} ⋯ X^{a_{γs}} and do not occur in X^{b_{δ_{1}}} ⋯ X^{b_{δ_{t}}}.

For any boolean multiplicative Thue system T it is helpful to consider the following graph M_{T} of monomials (cf. [5]). Its 2^{n} vertices are the monomials X^{I}, and two monomials X^{I}, X^{J} are linked by an edge if X^{I}X^{J} is one of the monomials of type (2) (after reductions by (1)). For the produced above system T_{n} we call an edge in M_{T_{n}} between X^{I} and X^{J} distinguished if X^{I}X^{J} = X_{1}. Lemma 3 Refutations for T_{n} correspond exactly to cycles in M_{T_{n}} which pass through 1 and have an odd number of distinguished edges. Proof Any refutation corresponds to a cycle (see definition 2) m_{0}, …, m_{N} and since −1 = −m_{0} = m_{N} = (m_{0}m_{1})(m_{1}m_{2}) ⋯ (m_{N−1}m_{N}), we conclude that among the edges m_{i−1}m_{i} of M_{T_{n}} there are an odd distinguished ones. Conversely, any cycle with an odd number of distinguished edges provides a refutation. Lemma 4 The degree of any refutation in T_{n} is at least Ω(n) (cf. e.g. lemma 5.9 [18]). Proof Take any refutation m_{0}, …, m_{N}. Denote by v_{1}, …, v_{N_{1}} ∈ (GF (2))^{6n} the exponent vectors of the (reduced) monomials (m_{0}m_{1}), (m_{1}m_{2}), …, (m_{N−1}m_{N}) ignoring all distinguished edges and preserving the order of the rest ones. Lemma 3 implies that v_{1} + ⋯ + v_{N_{1}} = (1, 0, …, 0). By lemma 2a) the weight of the vector v_{1} + ⋯ + v_{N_{1}} equals to 2n. For a certain ℓ_{1} ≤ N_{1} the weight of the vector v_{1} + ⋯ + v_{ℓ_{1}} equals to n. The vector v_{ℓ_{1}} is the exponent vector of a monomial m_{ℓ−1}m_{ℓ} for a certain ℓ ≥ ℓ_{1}. Then the exponent vector of the monomial m_{ℓ} = (m_{0}m_{1})(m_{1}m_{2}) ⋯ (m_{ℓ−1}m_{ℓ}) equals either to v_{1} + ⋯ + v_{ℓ_{1}} or to v_{1} + ⋯ + v_{ℓ_{1}} + (1, 0, …, 0). Lemma 2b) entails a lower bound Ω(n) on the degree of v_{1} + ⋯ + v_{ℓ_{1}}, that proves the lemma.

2 Lower Bound on Nullstellensatz Proofs

In [13] (see also [5]) a connection between Thue systems and membership problem for Thue ideals was exploited, and a double exponential lower bound for the latter problem was ascertained. Our situation is different since we study refutations (rather than the ideal membership problem), for which in general a single exponential upper bound is known ([2], [8]).

Convert any Thue system T (see section 1) into a boolean multiplicative polynomial ideal P ⊂ F [X_{1}, …, X_{n}] replacing each term σm (where σ ∈ {−1, 1} and m is a monomial) in (1) or (2) by the binomial 1 − σm. Evidently, T is satisfiable if and only if P is satisfiable. Denote by P_{n} = (1 − X_{1}^{2}, …, 1 − X_{n}^{2}, f_{1}, …, f_{t}) the polynomial ideal converted from T_{n}.

Theorem 1 Any Nullstellensatz refutation for P_{n} has the degree Ω(n) (over any field with the characteristic distinct from 2). Proof Let 1 = ∑ g′_{i}(1 − X_{i}^{2}) + ∑ g_{j}f_{j}. Consider a modified graph M_{P_{n}} with the same (as M_{T_{n}}) set of 2^{n} vertices (i.e. monomials). For each term um′ (where 0 ≠ u ∈ F) occurring in g_{j} and f_{j} = 1 − σm we draw an edge (m′m, m′) in M_{P_{n}} endowed with the weight u. Thus, the induced weight of its incident vertex m′ equals to u, and the induced weight of the vertex m′m equals to −σu. Clearly, no edges correspond to the polynomials 1 − X_{i}^{2}.

W.l.o.g. we can consider the connected component of M_{P_{n}} which contains the monomial 1. Observe that for every vertex of M_{P_{n}} (except for just 1) the sum of the induced weights by all the incident edges equals to 0, and for the vertex 1 this sum equals to 1. If the connected component has a cycle with an odd number of distinguished edges (m′X_{1}, m′) (they correspond to the polynomial 1 + X_{1}) then there is a cycle with the same property passing through 1, and we complete the proof of the theorem applying lemmata 3,4.

Now suppose on the contrary that each cycle has an even number of the distinguished edges. Then one can partition all the vertices (of the connected component) into two parts V_{0}, V_{1}. The set V_{0} consists of all the vertices reachable in M_{P_{n}} from 1 by paths with an even number of the distinguished edges. Then any distinguished edge links a vertex from V_{0} with a vertex from V_{1}. Any other edge has its incident vertices either both in V_{0} or in V_{1}.

We partition the sum of the weights (see above) induced by all the edges into Σ_{0} + Σ_{1} over the vertices from V_{0} and from V_{1}, respectively. Then each distinguished edge gives an equal contribution into both Σ_{0} and Σ_{1}. Every other edge gives the zero contribution into both Σ_{0} and Σ_{1}. Hence Σ_{0} = Σ_{1}. But on the other hand Σ_{1} = 0 and Σ_{0} = 1, which contradicts the supposition and proves the theorem.

Now we obtain a similar lower bound for more customary (see e.g. [3], [7], [6], [4], [14], [10]) boolean polynomial ideals (i.e. the ideals containing polynomials X_{i}^{2}−X_{i}, for all 1 ≤ i ≤ n, rather than X_{i}^{2}−1 as above). For each variable X_{i}, 1 ≤ i ≤ n making the linear transformation X_{i} → −2X_{i}+1 we transform the polynomials X_{i}^{2} − 1 to 4(X_{i}^{2} − X_{i}). Denote by P′_{n} ⊂ F [X_{1}, …, X_{n}] the system obtained by this transformation from P_{n} (evidently, it consists of the polynomials of degrees at most 6). Notice that P′_{n} is not necessary a binomial system (unlike P_{n}). Corollary 1 Any Nullstellensatz refutation for P′_{n} has the degree Ω(n) (again over any field with the characteristic distinct from 2).

One could also study boolean Thue systems relative the polynomials X_{i}^{2}−X_{i}, 1 ≤ i ≤ n, rather than X_{i}^{2}−1. Some advantage of these systems is that it is possible to consider them over arbitrary fields F unlike the multiplicative systems which were useless for the fields of characteristic 2 (see section 1). Definition 3 A boolean Thue system T′ is a family of polynomials of two types

X_{i}^{2} − X_{i}  1 ≤ i ≤ n  (3)
α′m′ − α′′m′′  (4)

where α′, α′′ ∈ F, m′, m′′ are monomials. Definition 4 A refutation of T′ is a sequence of reduced terms m_{0} = 1, m_{1}, …, m_{N} = 0 such that for any 1 ≤ i ≤ N there is α ∈ F and a monomial m such that m_{i−1} = αα′m m′, m_{i} = αα′′mm′′ for an appropriate polynomial of type (4).

Unfortunately, the next obtained for this system lower bound (which one can show by a straightforward induction) is weaker than the bound from theorem 1. Proposition 1 Consider a boolean Thue system in the variables X_{1}, …, X_{n}, Y_{1}, …, Y_{n} with the following polynomials of type (4):

X_{1}, Y_{1} − X_{1}, Y_{2} − Y_{1}X_{2}, …, Y_{n} − Y_{n−1}X_{n}, 1 − Y_{n}

Then any refutation of this system has the degree at least Ω(log n). Note that this bound is sharp.

Notice that one can test satisfiability of a boolean Thue system T′ in polynomial time. Indeed, among the terms occurring in (4), there should be a nonzero element of F (otherwise, just zeros would satisfy this system). Let it be a binomial α_{1}m_{1} − α_{2}, α_{2} ≠ 0. We start recursively augmenting a subset U of variables first including in it all the variables from m_{1} (the variables from U should attain the value 1 to satisfy T′). At a recursive step if all the variables from a term 0 ≠ α′m′ belong to U (this holds in particular if 0 ≠ α′m′ ∈ F) then add to U all the variables from m′′ (unless α′′ = 0, in this case the algorithm yields a refutation and terminates). Continue doing this way while U is augmented. When U can’t be augmented anymore, one can satisfy T′ putting 1 for the variables from U and putting 0 for the rest of the variables.

3 Lower Bound on Nullstellensatz Proofs for the Knapsack Problem over an Infinite Field

In [10] the lower bound [n/2] for Nullstellensatz proofs is shown for the polynomials {X_{i}^{2} − X_{i}, 1 ≤ i ≤ n, ∑_{1≤i≤n} C_{i}X_{i} − m} for any m and nonzero C_{1}, …, C_{n}, actually over any field of zero characteristic. Here we prove the lower bound n for the knapsack problem ∑_{1≤i≤n} C_{i}X_{i} − 1 for suitable C_{1}, …, C_{n} over an arbitrary infinite field F.

Proposition 2 For almost any γ_{1}, …, γ_{n} ∈ F any Nullstellensatz refutation for the system of polynomials {X_{i}^{2}− X_{i}, 1 ≤ i ≤ n, ∑_{1≤i≤n} γ_{i}X_{i} −1} has the degree at least n. Proof Let 1 = ∑ g_{i}(X_{i}^{2} − X_{i}) + g(∑ γ_{i}X_{i} − 1) for some γ_{1}, …, γ_{n} ∈ F. W.l.o.g. we can assume that g is multilinear. Suppose that deg g < n.

There exist not all zero constants {c_{η}}, η ∈ {0, 1}^{n} (in fact, they lie in the prime subfield of F) such that ∑_{η} c_{η}\overline{G}(η) = 0 (this identity holds for any multilinear polynomial \overline{G} of a degree less than n). Therefore, ∑_{η} _{\frac{c_{η}}{(∑_{i} γ_{i}η_{i}−1)}} = 0, where η = (η_{1}, …, η_{n}). The lat-

ter expression does not vanish for almost any γ_{1}, …, γ_{n} from an infinite field F.

4 Further Research and Open Questions

1) Over a field F of characteristic 2 which contains the field GF (4) one could almost literally repeat the construction from section 1 and theorem 1 with the following minor changes. The monomials (1) we replace by X_{i}^{3}, respectively, j_{1}, …, j_{n} ∈ {0, 1, 2} in (2), σ ∈ {1, θ, θ^{2}} where θ is a generator of the multiplicative group (GF (4))^{∗}. In the construction of the Thue system T_{n} one views a_{i}, b_{i} as the vectors from (GF (3))^{6n}, as the distinguished term in (2) takes θX_{1} (replacing −X_{1}). Then lemmas 1,2 go through, in lemma 3 one should replace “odd” by “not divisible by 3” and the corresponding graph M_{T_{n}} has now 3^{n} vertices. This leads to lemma 4. In the proof of theorem 1 we partition the vertices of the connected component (which contains 1) of the graph M_{P_{n}} (now the latter has 3^{n} vertices) into 3 parts, regarding d (mod 3), where d is the number of distinguished edges on a path from this vertex to 1.

But it is not clear how to prove corollary 1 if we’d like just to stick with the boolean equations X_{i}^{2} − X_{i}. Over the field GF (2) it is even less clear, how to conduct a similar to the above construction.

2) How to extend theorem 1 and corollary 1 to the polynomial calculus ([4], [14])?

3) How to obtain better (rather than logarithmic, see proposition 1) lower bounds for boolean Thue systems described at the end of section 2? It relates to “reversible” pebble games, in which it is allowed to propagate pebbles also backwards. Is it possible to adjust for them the known lower bounds (the best one is Ω(n/ log n)) for (the customary) pebble games (due to S. Cook, W.Paul, R. Tarjan et al.)? But actually boolean Thue systems seem to be more powerful then pebble games, and it would be interesting to obtain for them a linear lower bound.

Acknowledgement. The author is thankful to Sasha Razborov for drawing attention to this area.

References

[1] N. Alon. Eigenvalues and expanders. Combinatorica, 1986, 6, p. 83–96.

[2] D. Brownawell. Bounds for the degrees in the Nullenstellensatz. Ann. Math., 1987, 126, p. 577–591.

[3] P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, P. Pudlak. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc., 1996, 73, p. 1–26.

[4] S. Buss, R. Impagliazzo, J. Krajicek, P. Pudlak, A. Razborov, J. Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity, 1996/1997, 6, 3, p. 256–298.

[5] D. Bayer, M. Stillman. On the complexity of computing syzygies. J. Symb. Comput., 1988, 6, p. 135– 147.

[6] P. Beam, S. Riis. More on the relative strength of counting principles. Proc. DIMACS workshop on Feasible Arithmetic and Complexity of Proofs, 1996.

[7] P. Beame, S. Cook, J. Edmonds, R. Impagliazzo, T. Pitassi. The relative complexity of NP search problems. Proc. ACM STOC, 1995, p. 303–314.

[8] N. Fitchas, A. Galligo. Nullstellensatz effectif et Conjecture de Serre (Theoreme de Quillen-Suslin) pour le Calcul Formel. Math. Nachr., 1990, 149, p. 231–253.

[9] Z.Galil. On the complexity of regular resolution and the Davis-Putnam procedure. Theor. Comput. Sci., 1977, 4, p.23–46.

[10] R. Impagliazzo, P. Pudlak, J. Sgall. Lower bounds for the polynomial calculus and the Groebner basis algorithm. Preprint 1997.

[11] A. Lubotzky, R. Phillips, P. Sarnak. Ramanujan graphs. Combinatorica, 1988, 8, p. 261–277.

[12] G. Margulis. Explicit group-theoretical constructions of combinatorial schemes and their applications to the design of expanders and concentrators. Problems Inform. Transm., 1988, 24, p. 39–46.

[13] E. Mayr, A. Meyer. The complexity of the word problem for commutative semigroups and polynomial ideals. Adv. Math., 1982, 46, p. 305–329.

[14] A. Razborov. Lower bounds for the polynomial calculus, to appear in Computational Complexity.

[15] A. Seidenberg. Constructions in algebra. Trans. AMS, 1974, 197, p. 273–313.

[16] G.Tseitin. On the complexity of derivations in propositional calculus, in: Studies in mathematics and mathematical logic, vol. II, 1968, p. 115–125.

[17] A.Urquhart. Hard examples for resolution. J. ACM, 1987, 34, p. 209–219.

[18] A.Urquhart. The complexity of propositional proofs. Bull. Symb. Logic, 1995, 1, p. 425–467.