zbMATH — the first resource for mathematics

The intractability of resolution. (English) Zbl 0586.03010
In 1970, 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 S. A. Cook and 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.
Reviewer: A.Leitsch

03B35 Mechanization of proofs and logical operations
03D15 Complexity of computation (including implicit computational complexity)
03F20 Complexity of proofs
03B05 Classical propositional logic
68Q25 Analysis of algorithms and problem complexity
Full Text: DOI
[1] Barr, A.; Cohen, P.; Feigenbaum, E.A., (), Chapter 7
[2] Cook, S.A.; Reckhow, R.A.; Cook, S.A.; Reckhow, R.A., On the lengths of proofs in the propositional calculus, preliminary version, (), ACM sigact news, 6, 15-22, (1974), Final version in · Zbl 0375.02004
[3] Cook, S.A.; Reckhow, R.A., The relative efficiency of propositional proof systems, J. symbolic logic, 44, 1, 36-50, (1979) · Zbl 0408.03044
[4] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 1, 201-215, (1960) · Zbl 0212.34203
[5] Galil, Z., On the complexity of regular resolution and the Davis-Putnam procedure, Theoret. comput. sci., 4, 1, 23-46, (1977) · Zbl 0385.68048
[6] Garey, M.R.; Johnson, D.S., ()
[7] Justen, K., A note on regular resolution, Computing, 26, 1, 87-89, (1981) · Zbl 0431.03036
[8] Robinson, J.A., A machine oriented logic based on the resolution principle, J. ACM, 12, 23-41, (1965) · Zbl 0139.12303
[9] Tseitin, G.S., On the complexity of derivations in propositional calculus, (), 115-125
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.