Resolution remains hard under equivalence

The basis of this paper is the observation that for several proof systems f or propositional formulas in conjunctive normal form there are families of hard examples for which the shortest proof requires superpolynomially many steps. We will show that - under the assumption NP not equal coNP - it is i mpossible to transform formulas into a logically equivalent formula by addi ng polynomially many clauses such that it can be decided in polynomial time whether a clause is a consequence of the enlarged formula. This result esp ecially holds for resolution, i.e. for all polynomials p and q there exists a formula Phi is an element of CNF, such that for each equivalent formula Psi is an element of CNF with \Psi\ less than or equal to q(\Phi\) there is a clause n with Phi satisfies pi for which the shortest resolution proof P si proves (RES) pi requires more than p(\Phi\ + \pi\) resolution steps. (C) 1999 Elsevier Science B.V. All rights reserved.