The intractability of resolution (Q1071750)

In 1970, \textit{G. S. Tsejtin} [On the complexity of derivations in propositional calculus, Studies in Math. and Math. Logic II, 115-125 (1970)] proved that regular resolution for propositional logic is exponential; this means that there exists an infinite sequence of sets of clauses, whose minimal regular resolution trees are of exponential size. However, the complexity of general resolution (for propositional logic) remained unknown until now. Thus this paper is an important contribution to complexity theory, showing that propositional resolution is exponential. The sequence of sets of clauses establishing the exponential lower bound is defined by the so called pigeonhole principle; the clauses defined in this paper were also used by \textit{S. A. Cook} and \textit{R. A. Reckhow} [J. Symb. Logic 44, 36-50 (1979; Zbl 0408.03044)] for another purpose. Technically, the clauses are represented by rectangular schemata, which describe the position of positive and negative signs of the Boolean variables. Moreover, the author shows that the sequence of clause-sets \(PF_ n\) (whose resolution trees are at least of size \(c^ n\) for a constant c) can be proved by extended resolution in polynomial length (extended resolution is a method defined by Tsejtin). Therefore the tautologies \(PF_ n\) are only hard for resolution, and the complexity of the tautology problem for propositional logic (which is co- NP complete) remains unknown.