Generating Hard Tautologies Using Predicate Logic and the Symmetric
Group
Søren Riis 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 . 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 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
Available as |

Last modified: 2003-06-08 by webmaster.