BRICS RS-98-19 Riis & Sitharam: Generating Hard Tautologies … BRICS

Basic Research in Computer Science

Generating Hard Tautologies Using Predicate Logic and the Symmetric Group

Søren Riis Meera Sitharam BRICS Report Series RS-98-19 ISSN 0909-0878 September 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/19/

Generating hard tautologies using predicate logic and the symmetric group

Søren Riis^{∗}^{†} Meera Sitharam ^{‡}^{§}

September 1998

Abstract

We introduce methods to generate uniform families of hard propositional tautologies. The tautologies are essentially generated from a single propositional formula by a natural action of the symmetric group S_{n}.

The basic idea is that any Second Order Existential sentence Ψ can be systematically translated into a conjunction ϕ of a finite collection of clauses such that the models of size n of an appropriate Skolemization Ψ̃ are in one-to-one correspondence with the satisfying assignments to ϕ_{n}: the S_{n}-closure of ϕ, under a natural action of the symmetric group S_{n}. Each ϕ_{n} is a CNF and thus has depth at most 2. The size of the ϕ_{n}’s is bounded by a polynomial in n. Under the assumption NEXPTIME ≠ co-NEXPTIME, for any such sequence ϕ_{n} for which the spectrum S := {n : ϕ_{n} satisfiable} is NEXPTIME-complete, the tautologies ¬ϕ_{n∉S} do not have polynomial length proofs in any propositional proof system.

Our translation method shows that most sequences of tautologies being studied in propositional proof complexity can be systematically generated from Second Order Existential sentences and moreover, many natural mathematical statements can be converted into sequences of propositional tautologies in this manner. We also discuss algebraic proof complexity issues for such sequences of tautologies. To this end, we show that any Second Order Existential sentence Ψ can be systematically translated into a finite collection of polynomial equations Q̄ = 0 such that the models of size n of an appropriate skolemization Ψ̃ are in one-to-one correspondence with the solutions to Q̄_{n} = 0: the S_{n}-closure of Q̄ = 0, under a natural action of the symmetric group S_{n}. The degree of Q̄_{n} is the same as that of Q̄, and hence is independent of n, and the number of variables is no more than a polynomial in n. Furthermore, using results in [19] and [20], we briefly describe how, for the corresponding sequences of tautologies ϕ_{n}, the rich structure of the S_{n} closed, uniformly generated, algebraic systems Q̄_{n} has profound consequences on on the algebraic proof complexity of ϕ_{n}.

1The International PhD Research School at BRICS, Aarhus, Denmark; Email:

smriis@daimi.aau.dk

2Part of this work was done while visiting the Fields Institute, Toronto, Canada 3CISE Department, University of Florida, Gainesville, FL 32611-6120; Email:

sitharam@cise.ufl.edu

4Supported in part by NSF Grant CCR 94-09809.

I Introduction

Algebraic deductive systems have been used in automatic (First Order) theorem proving for several decades. Roughly speaking, these systems translate the axioms (First Order logic sentences), and the theorem to be proved, into polynomial equations, in such a way that the proof of the theorem can be obtained as a proof of membership in the ideal generated by these polynomial equations. Several algorithms for such equational reasoning have been developed, based on Cylindrical Algebraic Decomposition, Hilbert’s Nullstellensatz, Gröbner bases, Wu-Ritt Characteristic sets, etc., and have turned out to be effective, e.g, for geometry theorem proving [6], [9], [12], [21]. Many of these algebraic deductive systems have the advantage of being automatizable in that the time taken to find the proof is strongly related to the length of the proof.

More recently, algebraic deductive systems have been employed in the context of proving lower bounds on the proof complexity of propositional tautologies [4], [5], [7], [8]. Showing the nonexistence of polynomial (in n) length proofs for a sequence of tautologies ϕ_{n}, is directly linked to the NP ≠ co-NP question: the link becomes stronger with the strength of the proof system used.

In this paper, we first give a systematic method of translating an Existential Second Order sentence Ψ into a sequence of depth 2 polynomial size propositional formulae ϕ_{n} such that ϕ_{n} is satisfiable (or ¬ϕ_{n} is not a tautology), if and only if a Ψ has a model of size n.

We give an analogous algebraic version of this: a systematic method of translating an Existential Second Order sentence Ψ into a polynomial system Q̄ such that the S_{n}-closure Q̄_{n} of Q̄ has a solution if and only if Ψ has a model of size n. Since Q̄_{n} is uniformly generated by S_{n}-closure, its degree is independent of n, and its number of variables is bounded by a polynomial in n.

More specifically, the system Q̄ is based on an appropriate (nonunique) Skolemization Ψ̃ of Ψ, and the models M ⊧ Ψ̃ of size n are directly related to the ideal I_{Ψ,n} generated by the polynomials in Q̄_{n} In particular, there is a 1-1 correspondence between models of Ψ̃ of size n and points on the (discrete) algebraic variety defined by I_{Ψ,n}.

Krajicek has pointed out (personal communication) that Paris and Wilkie applied a translation procedure very similar to ours. This is indeed correct. They introduced this translation in their proof of Theorem 26 (see [14]) in the setting of non-standard models for Bounded Arithmetic. The Paris-Wilkie translation shows how bounded first order formulas can be translated into a sequence of polynomial size bounded depth propositional formulas (see for example [10] for a definition of this). Paris and Wilkie do not consider the case where one is translating formulas involving uninterpreted function symbols. Actually in our case both function symbols as well as relational symbols are uninterpreted. This is crucial for getting the S_{n}-closure properties we are using. Our idea of introducing uninterpreted functions (via Skolemization) plays a crucial role. Without this idea we would NOT get a sequence of polynomial equations of bounded degree. Neither would we get a translation leading to a finitely generated S_{n}-closed sequence of satisfiability problems.

Our translation shows that many natural mathematical problems can be converted into questions of propositional satisfiability, and thence to questions about the existence of solutions to polynomial equations. For example, the question of whether there is a nilpotent group of size n is identical to the question of whether there is a model of size n for the Existential Second Order statement “the universe is a nilpotent group”. Clearly, many natural problems in algebra, number theory, graph theory, or combinatorics can be phrased in this manner.

Our translation highlights the fact that many tautologies used for showing algebraic proof complexity lower bounds, such as various matching principles, versions of the pigeonhole principle, and primality principle [4], [5], [7], [11] can indeed be obtained from natural Second Order Existential statements. We illustrate this using examples.

More significantly, we introduce a method to systematically generate hard propositional tautologies from Second Order Existential sentences. The method relies on sentences that have a hard spectrum and we show how to generate uniform sequences of tautologies that have no polynomial length proofs provided NEXPTIME ≠ co-NEXPTIME.

In addition, we briefly sketch how this method works for algebraic proof systems such as Nullstellensatz and Polynomial Calculus proof systems (unconditionally, with no additional assumptions from complexity theory). The sequences of propositional formulae ϕ_{n} obtained using our translation have a rich algebraic structure due to the symmetries in the corresponding polynomial systems. This symmetry permits the representation theory of S_{n} to be used in analyzing the proof complexity of the corresponding tautologies, in various algebraic deductive systems.

Ajtai was the first to consider and analyse uniform S_{n}-closed families of linear equations [1], [2], [3]. In [19], [20] we prove various new and rather deep theorems related to algebraic proof complexity. These theorems strongly relies on the fact that our translation gives finitely generated S_{n}-closed systems of propositional formulas (polynomial equations).

II The Translation

We first develop the required notation and definitions. Let ∃_{r} denote the second order existential quantifier for r-ary relations. Let ∃′_{s} denote the Second Order Existential quantifier for s-ary functions. Let ∃ and ∀ denote the first order quantifiers. A pure atomic formula is of the form: R(t_{1}, …, t_{l}) or f(t_{1}, t_{2}, …, t_{l}) = s or t = s where R is an l-ary relation and f is an l-ary function and s, t, t_{1}, …, t_{l} are (not necessarily distinct) variables. A Second Order Existential sentence Ψ is strict (recalling the class MaxSNP [13]) if it is of the following form:

∃_{r_{1}}R_{1} … ∃_{r_{u}}R_{u}∃′_{s_{1}}f_{1} … ∃′_{s_{v}}f_{v}∀z_{1}, …, z_{w} η(z⃗)

where η(z⃗) := η(z_{1}, z_{2}, …, z_{w}) is a Boolean combination of pure atomic formulas. The strongest results are achieved if we assume η is in Conjunctive Normal Form. Let Ψ_{n} denote the sentence which is achieved from Ψ by restricting all quantifiers to the universe {1, 2, …, n}.

For an arbitrary Second Order Existential sentence (on prenex normal form)

Ψ = ∃_{r_{1}}R_{1} … ∃_{r_{u}}R_{u}∃′_{s_{1}}f_{1} … ∃′_{s_{v}}f_{v} η̃

where η̃ :≡ ∀z_{1}∃y_{1} … ∀z_{w}∃y_{w} η(z_{1}, y_{1} …, z_{w}, y_{w}); a corresponding strict version Ψ̃ is obtained by Skolemization: we eliminate all first order existential quantifiers by introducing Skolem functions g such that

Ψ̃ := ∃_{r_{1}}R_{1} … ∃_{r_{u}}R_{u}∃′_{s_{1}}f_{1} … ∃′_{s_{v}}f_{v}∃′_{1}g_{1} … ∃′_{w}g_{w}η′

where η′ ≡ η(z_{1}, g_{1}(z_{1}) …, z_{w}, g_{w}(z_{1}, …, z_{w})). It should be noticed that different Skolemizations in general might lead to different Ψ̃.

Next, consider the ring IF[x_{j,e_{j}} : e_{j} ∈ {1, …, n}^{r_{j}}, 1 ≤ j ≤ u] of polynomials over a field IF and the vector space Π_{n,d} spanned by those polynomials of degree at most d. Notice that this vector space is closed under the following action of the symmetric group S_{n}: Q(x_{j,e_{j}}) ∈ Π_{n,d} ⇒ ∀π ∈ S_{n}π(Q(x_{j,e_{j}})) ∈ Π_{n,d}, where π(Q(x_{j,e_{j}})) := Q(x_{j,π(e_{j})}), and for e_{j} := (e_{1,j}, …, e_{r_{j},j}) ∈ {1, …, n}^{r_{j}}, π(e_{j}) is the natural action defined as: (π(e_{1,j}), …, π(e_{r_{j},j})). In general, given a set of polynomials Q̄ where Q̄ := {Q_{1}, …, Q_{m}}, each Q_{i} ∈ Π_{l,d}, for some fixed l, we say that a sequence of polynomial systems Q̄_{n} is S_{n}-closed and uniformly generated from Q̄, if for all n, Q̄ ⊆ Q̄_{n}, and Q_{i} ∈ Q̄_{n} ⇒ π(Q_{i}) ∈ Q̄_{n} ∀π ∈ S_{n}.

We are now ready to state our translation result.

Theorem 1 Let Ψ be a Second Order Existential Sentence and let Ψ̃ be a strict version obtained by a (non-unique) Skolemization. Then there is a sequence of propositional formulae ϕ_{Ψ̃,n} and a polynomial system Q̄Ψ̃ ∈ Π_{l,d}, for some constants l and d depending only on Ψ, such that the following hold.

1. Each ϕ_{Ψ̃,n} is a CNF (i.e. conjunctions of disjunctions of literals and negation of literals) such that there is a 1-1 correspondence between the models of Ψ̃ of size n and satisfying truth assignments to ϕ_{Ψ̃,n}.

2. For each n, the conjunction of clauses that form ϕ_{Ψ̃,n} is closed under the group action S_{n} and is generated by closing a fixed, finite set ϕ of clauses under a natural action of the symmetric group S_{n}. (Some of these clauses are formal clauses containing n literals).

3. Let Q̄_{Ψ̃,n} ∈ Π_{n,d} be a S_{n}-closed sequence of polynomial systems uniformly generated from Q̄Ψ̃ (hence Q̄_{Ψ̃,n} has degree d independent of n, and has a number of variables that is polynomially bounded in n). There is a 1-1 correspondence between the models of Ψ̃ of size n and the solutions to Q̄_{Ψ̃,n} = 0.

4. Let ϕ_{Ψ̃,n} be as above. Then Ψ does not have a model of size n if and only if ϕ_{Ψ̃,n} not is satisfiable if and only if ¬ϕ_{Ψ̃,n} is a tautology if and only if there is no solution to Q̄_{Ψ̃,n} = 0

Proof. Let Ψ̃ be a strict Second Order Existential sentence in which the quantifier-free first order part η is in CNF. We translate the sequence Ψ̃_{n} into a sequence of propositional formulas as follows:

For given n we fix the collection of Boolean variables which consists of:

q_{i_{1},i_{2},...,i_{r_{1}}}^{(1)}, …, q_{i_{1},i_{2},...,i_{ru}}^{(u)} as well as p_{i_{1},i_{2},...,i_{s_{1}},i_{s_{1}+1}}^{(1)}, …, p_{i_{1},i_{2},...,i_{sv+1}}^{(v)} where each i_{j} ∈ {1, 2, …, n}.

Translate the sequence Ψ̃_{n} into a sequence of propositional formulas as follows:

For each selection i_{1}, i_{2}, …, i_{w} ∈ {1, 2, …, n} we let γ := η_{i_{1},i_{2},...,i_{w}} denote the propositional formula which appears by performing the following operations.

(1) Replacing each z_{j} in η by the number i_{j}.

(2) Replace each atomic formula R_{l}(j_{1}, j_{2}, …, j_{r_{l}}) in γ by q_{j_{1},j_{2},...,j_{r_{l}}}^{(l)} where j_{1}, … are numbers ∈ {1, 2, …, n} after performing the replacement in (1).

(3) Replace each atomic formula f_{l}(j_{1}, j_{2}, …, j_{s_{l}}) = j_{s_{l}+1} in γ by p_{j_{1},j_{2},...,j_{r_{l}},j_{s_{l}+1}}^{(l)} where j_{1}, … are numbers ∈ {1, 2, …, n} after performing the replacement in (1). Thus, removing the universal quantifier on the variables z_{i} of η gives us a conjunction of a set C_{n} of O(n^{w}) CNF formulae of fixed length independent of n. Notice that for any n, the set C_{n} can be obtained uniformly by the natural action of S_{n} on the fixed set C_{l} of clauses,

where l ≤ ∑_{j}^{u} r_{u} + ∑_{j}^{v}(s_{v} + 1).

To complete the process, we need to assert that the f_{m} are functions, i.e, that they take exactly one value. To do this, we first supplement the set of fixed length formulae in C_{n} by additional simple clauses of the form ¬p_{i_{1},i_{2},...i_{sm},j}^{(m)} ∨ ¬p_{i_{1},i_{2},...i_{sm},j′}^{(m)}, one for each j, j′ ∈ {1, 2, …, n} with j ≠ j′ and for each i_{1}, i_{2}, … ∈ {1, 2, …, n}. Thus for each n, the resulting collection D_{n} of fixed length, CNF formulae can still be obtained by S_{n}-closure of the fixed set D_{l} of formulae.

Finally to assert that the function f_{m} takes at least 1 value, for each and for each i_{1}, i_{2}, … ∈ {1, 2, …, n}, we need to include into the collection D_{n} formal clauses of the type ∨_{j}p_{i_{1},i_{2},...i_{sm},j}^{(m)}. Such clauses vary with n (as does the length), however, in a uniform manner. Again, for each n, the resulting collection E_{n} of formal CNF formulae can still be obtained by S_{n}-closure of the fixed set E_{l} of formal formulae.

Now ϕ_{Ψ̃,n} is taken to be the conjunction This formula ϕ_{Ψ̃,n} is a conjunction of CNF’s and formal disjunctive clauses. in E_{n}. Thus (letting n = l) ϕ_{Ψ̃,l} can be reduced to a finite conjunction of formal clauses and the clauses in ϕ_{Ψ̃,n} are generated from these formal clauses by an application of the symmetric group S_{n}. Hence ϕ_{Ψ̃,n} is a conjunction of a set of polynomially many clauses. Clearly, from any satisfying assignment for ϕ_{Ψ̃,n} we can read-off a model of Ψ_{n}.

Next we notice that the same idea can be used to produce a system of polynomial equations, one for each clause in ϕ_{Ψ̃,n}, over any given field IF, by replacing each disjunction x ∨ y by the polynomial (1 − x).(1 − y), ¬x by the polynomial x and replacing the formal disjunction ∨_{j}p_{i_{1},i_{2},...i_{sm},j}^{(m)} - arising from functions f^{m} in Ψ̃ - by a formal sum of the form Σ_{j} p_{i_{1},i_{2},...,i_{sm},j}^{(m)} − 1. This replacement is not valid for general disjunctions, but works in this particular case due to the presence of the other disjunctions ¬p_{i_{1},i_{2},...i_{sm},j}^{(m)} ∨ ¬p_{i_{1},i_{2},...i_{sm},j′}^{(m)}, for each distinct pair j, j′. Finally we add for each variable x the equation x^{2} − x = 0.

The closure under S_{n} ensures that different solutions to Q̄_{Ψ̃,n} = 0 (that are not isomorphic under S_{n}) correspond to non-isomorphic models of Ψ̃. In fact, the number of non-isomorphic models M ⊧ Ψ̃_{n} is inversely related to the size of the ideal I_{Ψ̃,n} generated by the polynomials in Q̄. Clearly the ideals I_{Ψ̃,n} are closed under S_{n} as well. Knowledge of I_{Ψ̃,n} allows us uniquely to determine all models of Ψ̃_{n}, since there is a 1-1 correspondence between models of Ψ̃_{n} and points on the algebraic variety defined by I_{ψ,n}.

III Some Examples

Example (dense linear ordering)

Fix the language L = L(R, f) where R is a binary relation symbol and f is a binary function symbol. Consider the L-sentence: η ≡ (∀x, y, z (R(x, y)∧R(y, z) ⇒ R(x, z))∧(∀x, y(R(x, y) ⇒ (¬R(y, x)∨x = y))) ∧(∀x, y(R(x, y)∨R(y, x)∨x = y)) ∧∀x, y(R(x, y) ⇒ R(x, f(x, y))∧ R(f(x, y), y)).

The sentence is a formalization of “R is a linear ordering whose denseness is witnessed by f”. The sentence ∃R∃fη is a strict second order existential sentence.

We show how the translation works on this example. Rewrite the L(R, f)-sentence as: η ≡ ∃R∃f ∀i, j, k[(¬R(i, j) ∨¬R(j, k) ∨ R(i, k))∧ (¬R(i, j) ∨ ¬R(j, i) ∨ i = j) ∧(R(i, j) ∨ R(j, i) ∨ i = j) ∧(¬R(i, j) ∨ (R(i, f(i, j)) ∧¬R(j, f(i, j)) ∧ R(f(i, j), j)))].

Now introduce variables x_{ij} and y_{ijk} with the intended idea that x_{ij} = 1 ⟺ R(i, j) and y_{ijk} = 1 ⟺ f(i, j) = k. This gives polynomial equations: x_{ij}x_{jk}(1 − x_{ik}) = 0 for all i, j, k, x_{ij}x_{ji} = 0 for all i ≠ j, (1 − x_{ij})(1 − x_{ji}) = 0 for all i ≠ j, and x_{ij}y_{ijl}(1 − x_{il}x_{lj}) = 0 for all i, j, l. Besides we add the equations: x_{ij}^{2} − x_{ij} = 0 for all i, j, y_{ijk}^{2} − y_{ijk} = 0 for all i, j, k,

∑_{l} y_{ijl} − 1 = 0 for all i, j, and y_{ijk}y_{ijl} = 0 for all i, j, k ≠ l.

These equations can be simplified and some equations (like y_{ijk}^{2}−y_{ijk} = 0) are superfluous because they can be derived from the other equations. A natural simplification gives the following system of equations: x_{ij}x_{jk}x_{ki} = 0 for i ≠ k, j, x_{ij} + x_{ji} − 1 = 0 for all i, j,

x_{ij}y_{ijl}(1 − x_{il}x_{lj}) = 0 for i, j, l, ∑_{l} y_{ijl} − 1 = 0 for all i, j,

x_{ij}^{2} − x_{ij} = 0 for all i, j, and y_{ijk}y_{ijl} = 0 for all i, j, k ≠ l Finally we can get a fixed set of generating equations. For example, y_{ijk}y_{ijl} = 0 for all i, j, k ≠ l is generated (under the action of S_{n}) by the 6 equations for indices in {1, 2, 3, 4}: y_{123}y_{124} = 0, y_{112}y_{113} = 0, y_{111}y_{112} = 0, y_{121}y_{122} = 0, y_{121}y_{123} = 0, y_{122}y_{123} = 0. ♣ The next example shows how one can treat constants in a translation. More significantly, it shows how a sequence of tautologies, commonly studied in the context of algebraic proof complexity lower bounds [4],[5],

[7] can be obtained from a Second Order sentence using this translation.

Example (onto-PHP): Fix the language L = L(f, c). Consider the Second Order Universal sentence in the language L.

Ψ ≡ ∀f ((∃x, yf(x) = f(y) ∧ x ≠ y) ∨ (∃xf(x) = c)).

This statement is a formalization of the principle that there is no onto map f : U → U which avoids the point {c}. The negation η is on the form:

η ≡ ∃f ((∀i, j f(i) = f(j) → i = j) ∧ (∀i f(i) ≠ c)).

Now introduce variables x_{ij} and y_{j} with the intention that x_{ij} = 1 ↔ f(i) = j and y_{j} = 1 ↔ c = j. This gives the equations: x_{ij}x_{ik} = 0 for all i, j ≠ k x_{ij}y_{j} = 0 for all i, j, ∑_{j} x_{ij} −1 = 0 for all i , y_{i}y_{j} = 0 for all i, j and the equation ∑_{j} y_{j} −1 = 0.

A different set of equations for the onto-PHP (more specifically onto-PHP_{n}^{n−1}) was considered in [4],[5],[7]. This system of equations essentially appears by letting y_{n} = 1. Notice that this system is only closed under S_{n−1}. Furthermore, other sequences of tautologies studied in proof complexity, such as various matching principles, the primality principle [4],[5], [7], [11] etc. can also be obtained from Second Order sentences using our translation. ♣

IV Construction of Hard Tautologies

One of the most fundamental questions in the theory of proof complexity is the following: how to obtain families of tautologies which do not have short proofs in a given system of propositional calculus?

First, consider the opposite question. How to obtain easy tautologies? One easy class of tautologies arises from a Second Order Universal sentence Ψ which is a tautology of predicate logic. This happens when Ψ is valid in all models, i.e. not only is it valid in all finite models, but also holds in all infinite models. We call such tautologies absolute tautologies. Their importance was noticed in [15], [16], [17] and [18] in the setting of Bounded Arithmetic. The term “absolute” is borrowed from forcing in set theory. Absolute tautologies (in non-standard models) always remain true and are preserved in generic extensions of the universe. The corresponding sequence of propositional tautologies ϕ_{n} are easy to prove: essentially one can take the finite proof in predicate logic and turn it into a proof in propositional calculus. With the right stock of rules one can achieve this in a constant number of steps.

Now consider tautologies like the pigeonhole principle. This holds for finite models, but fails for infinite models. This already suggests that these tautologies are somewhat harder to prove. For such tautologies there is no longer a proof in predicate logic so different n’s require different treatments. On the other hand tautologies like the pigeonhole principle are still provable in a uniform way.

One way of constructing hard sequences of tautologies is to ensure that different values of n require distinctly different proofs. To do this, we consider Second Order Existential sentences Ψ for which the spectrum S := {n ∈ N : ∃M ⊧ Ψ_{n}} has high complexity. The proof of the following theorem formalizes this observation (the proof is fairly straightforward).

Theorem 2 Consider a Second Order Existential sentence Ψ for which the spectrum S := {n ∈ N : ∃M ⊧ Ψ_{n}} is NEXPTIME-complete. (Here we assume that the input is n, coded in binary). For any Skolemization Ψ̃, obtain the sequence of propositional formulae ϕ_{Ψ̃,n} as in Theorem 1. Now the sequence of propositional tautologies {¬ϕ_{Ψ̃,n}}_{n∉S} does not have polynomial (in n) length proofs (in any propositional proof system), unless NEXPTIME = co-NEXPTIME.

Next we briefly sketch a related method of generating unconditionally hard propositional tautologies, based on our translation. This method applies only to algebraic proof systems in particular, the Nullstellensatz system (NS) and the Polynomial Calculus system (PC) studied in the context of proof complexity lower bounds [4], [5], [7]. The idea behind NS and PC is to translate the given propositional tautology ϕ_{n} into an equivalent system of polynomial equations Q̄(x̄) = 0 over some field IF in the standard manner described in the proof of Theorem 1. The task of proving ϕ_{n} can thus be rephrased as the task of showing that Q̄(x̄) = 0 does not have a 0/1-solution over IF. According to a weak version of Hilbert’s Nullstellensatz, this is equivalent to showing that the ideal generated by Q̄ ∪ I (where I := {x^{2} − x, x variable}) contains the constant polynomial 1. An NS-proof is a list of witnessing polynomials P̄ such that ∑ P_{i}Q_{i} = 1, where P_{i} ∈ P̄ and Q_{i} ∈ Q̄ ∪ I. The degree of the proof is the maximum degree of the witnessing polynomials P̄, and acts as a natural proof complexity measure: a constant degree d NS proof implies that one can find the proof in time O(n^{O(d)}), simply by solving a linear system to obtain the coefficients of the witnessing polynomials P_{i}. Notice that the number of variables in the system Q̄ is a trivial upper bound on the degree of the NS proof since the polynomials x^{2} −x for each variable x have been added to Q̄. See [8] for a description of PC proofs.

The closure under S_{n} combined with the uniformity allows us to extract strong lower bounds on the degree as well as on the size of Nullstellensatz proofs as well as Polynomial Calculus proofs. Our analysis relies on the structure of the sequence of linear spans U_{n} of the S_{n}-closed, sequences Q̄_{n} ∈ Π_{n,d} generated from a fixed polynomial system Q̄ ∈ Π_{l,d} obtained in Theorem 1. These vector spaces that are also closed under the natural action of S_{n} are so-called IFS_{n} modules, studied extensively in the representation theory of S_{n}. In [19], we provide a non-traditional analysis of the structure of uniformly generated sequences of IFS_{n} modules for fields IF of characteristic 0. The gist of these results is that complete and precise decomposition of these module sequences into irreducible modules (beyond isomorphism types) can be uniformly specified, and as a result there is a single polynomial p(n) that captures the dimension of such module sequences for all but finitely many singular values of n, and moreover, for these singular n, the dimension is bounded above by p(n).

References

[1] Ajtai, M.: The independence of the modulo p counting principles. In Proceedings of the 26th ACM STOC, 402-411 (1994)

[2] Ajtai, M.: On the existence of modulo p cardinal functions, in: Feasible Mathematics II, eds. P. Clote and J. Remmel, Birkhauser. 1-14 (1994)

[3] Ajtai, M.: Symmetric systems of linear equations modulo p, TR94-015 of the Electronic Colloquium on Computational Complexity (1994)

[4] Beame, P., Impagliazzo, R., Krajicek, J., Pitassi, T., Pudlak, P.: Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proceedings of the London Mathematical Society 73(3) 1-26 (1996)

[5] Beame, P., Riis, S.: More on the relative strength of counting principles. In: Proceedings of the DIMACS workshop on Feasible Arithmetic and Complexity of Proofs, (1996)

[6] G.E. Collins: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition, In: Lect. Notes in CS, 33, 134-183 (1975)

[7] Buss, S., Krajicek, j,. Pitassi, T., Razborov, A., Sergal, J.: Polynomial bound on Nullstellensatz for counting principles. To appear in Computational Complexity (1997)

[8] Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the 28th ACM STOC 174-183 (1996)

[9] Chou, S. C., Gao, X. S., and Zhang, J. Z., A method of solving geometric constraints, Wichita State University, Tech. Rep, Dept. of Computer Sci., (1996)

[10] Krajicek, J.:Bounded Arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press (1995)

[11] Krajicek, J.: On the degree of ideal membership proofs from uniform families of polynomials over a finite field (manuscript)

[12] McCune, W., Padmanablan, R.: Automated deduction in equational logic and cubic curves. Lecture Notes in Computer Science, 1095 Springer-Verlag, Berlin (1996)

[13] Papadimitriou, C.: Computational Complexity, Addison-Wesley, (1994)

[14] Paris, J., Wilkie, A.: Counting Problems in Bounded Arithmetic, in: Methods in Mathematical Logic, LNM 1130, 317-340, Springer-Verlag (1985)

[15] Riis, S.: Making infinite structures finite in models of Second Order Bounded Arithmetic. In: Arithmetic, proof theory and computorial complexity, 289-319, Oxford: Oxford University Press 1993

[16] Riis, S.: Independence in Bounded Arithmetic. DPhil dissertation, Oxford University (1993)

[17] Riis, S.: Count(q) does not imply Count(p): Annals of Pure and Applied Logic, 90(1-3):1-56, (1997)

[18] Riis, S.: Count(q) versus the pigeon-hole principle. Archive for Mathematical Logic 36 157-188 (1997)

[19] Riis, S., Sitharam, M: Permutation modules and their uniformly generated submodules.

[20] Riis, S., Sitharam, M: Manuscript in preparation. Incomplete version appear as technical report TR97-048 of the Electronic Colloquium on Computational Complexity, http://www.eccc.unitrier.de/pub/eccc (1997)

[21] Ruiz, O.E., and Ferreira, P.M.: Algebraic geometry and group theory in geometric constraint satisfaction for computer-aided design and assembly planning, In: IIE Transactions on Design and Manufacturing, 28, 281-294, (1996)

Recent BRICS Report Series Publications

RS-98-19 Søren Riis and Meera Sitharam. Generating Hard Tautologies Using Predicate Logic and the Symmetric Group. September 1998. 13 pp.

RS-98-18 Ulrich Kohlenbach. Things that can and things that can’t be done in PRA. September 1998. 24 pp.

RS-98-17 Roberto Bruni, José Meseguer, Ugo Montanari, and Vladimiro Sassone. A Comparison of Petri Net Semantics under the Collective Token Philosophy. September 1998. 20 pp. To appear in 4th Asian Computing Science Conference, ASIAN ’98 Proceedings, LNCS, 1998.

RS-98-16 Stephen Alstrup, Thore Husfeldt, and Theis Rauhe. Marked Ancestor Problems. September 1998.

RS-98-15 Jung-taek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the Overhead of ML Exceptions by Selective CPS Transformation. September 1998. 31 pp. To appear in the proceedings of the 1998 ACM SIGPLAN Workshop on ML, Baltimore, Maryland, September 26, 1998.

RS-98-14 Sandeep Sen. The Hardness of Speeding-up Knapsack. August 1998. 6 pp.

RS-98-13 Olivier Danvy and Morten Rhiger. Compiling Actions by Partial Evaluation, Revisited. June 1998. 25 pp.

RS-98-12 Olivier Danvy. Functional Unparsing. May 1998. 7 pp. This report supersedes the earlier report BRICS RS-98-5. Extended version of an article to appear in Journal of Functional Programming.

RS-98-11 Gudmund Skovbjerg Frandsen, Johan P. Hansen, and Peter Bro Miltersen. Lower Bounds for Dynamic Algebraic Problems. May 1998. 30 pp.

RS-98-10 Jakob Pagter and Theis Rauhe. Optimal Time-Space Trade-Offs for Sorting. May 1998. 12 pp.

RS-98-9 Zhe Yang. Encoding Types in ML-like Languages (Preliminary Version). April 1998. 32 pp.