Resolution remains hard under equivalence Original Research Article

The basis of this paper is the observation that for several proof systems for 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≠coNP – it is impossible to transform formulas into a logically equivalent formula by adding polynomially many clauses such that it can be decided in polynomial time whether a clause is a consequence of the enlarged formula. This result especially holds for resolution, i.e. for all polynomials p and q there exists a formula Φ∈CNF, such that for each equivalent formula Ψ∈CNF with |Ψ|⩽q(|Φ|) there is a clause π with Φ⊨π for which the shortest resolution proof Ψ⊢RESπ requires more than p(|Φ|+|π|) resolution steps.