Generating Hard Tautologies Using Predicate Logic and the Symmetric Group

Resumé

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 Sn.
The basic idea is that any Second Order Existential sentence Psi can be systematically translated into a conjunction phi of a finite collection of clauses such that the models of size n of an appropriate Skolemization Psi~   are in one-to-one correspondence with the satisfying assignments to phi_n: the Sn-closure of phi, under a natural action of the symmetric group Sn. Each phi_n is a CNF and thus has depth at most 2. The size of the phi_n's is bounded by a polynomial in n. Under the assumption NEXPTIME |= co- NEXPTIME, for any such sequence phi_n for which the spectrum S := {n : phi_n satisfiable} is NEXPTIME-complete, the tautologies not phi_(n not in 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  Psi    can be systematically translated into a finite collection of polynomial equations Q = 0 such that the models of size n of an appropriate skolemization Psi~   are in one-to-one correspondence with the solutions to Qn = 0: the Sn-closure of Q = 0, under a natural action of the symmetric group Sn. The degree of Qn 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 phi_n, the rich structure of the Sn closed, uniformly generated, algebraic systems Qn has profound consequences on the algebraic proof complexity of phi_n.