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
.
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 
: the -closure of , under a
natural action of the symmetric group . Each is a CNF and thus
has depth at most 2. The size of the 's is bounded by a polynomial
in n. Under the assumption NEXPTIME 
co-NEXPTIME, for any
such sequence for which the spectrum 
is NEXPTIME-complete, the tautologies
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
such that the models of size n of an appropriate skolemization
are in one-to-one correspondence with the solutions to
: the -closure of , under a natural action of
the symmetric group . The degree of 
is the same as that of
, and hence is independent of n, and the number of variables is no
more than a polynomial in n. Furthermore, we briefly describe how, for the
corresponding sequences of tautologies , the rich structure of the
closed, uniformly generated, algebraic systems has profound
consequences on on the algebraic proof complexity of
Available as PostScript, PDF, DVI.