The intractability of resolution
type: Item
instance of: scholarly article
title: The intractability of resolution
zbMATH Open document ID: 0586.03010
DOI: 10.1016/0304-3975(85)90144-6
author: Armin Haken
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B05
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 3939322
zbMATH Keywords: complexity of general resolution
zbMATH Keywords: propositional logic
zbMATH Keywords: exponential lower bound
zbMATH Keywords: pigeonhole principle
zbMATH Keywords: extended resolution
zbMATH Keywords: tautology problem
reviewed by: Alexander Leitsch
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90144-6
OpenAlex ID: W2069767473
Wikidata QID: Q56224983
cites work: Q4152212
cites work: The relative efficiency of propositional proof systems
cites work: A Computing Procedure for Quantification Theory
cites work: On the complexity of regular resolution and the Davis-Putnam procedure
cites work: Q4198056
cites work: A note on regular resolution
cites work: A Machine-Oriented Logic Based on the Resolution Principle
DBLP publication ID: journals/tcs/Haken85
Recommended article: Q4699289
Recommended article: Proofs as Games
Recommended article: Theory and Applications of Models of Computation
Recommended article: The complexity of Gentzen systems for propositional logic
Recommended article: Resolution proofs of generalized pigeonhole principles
Recommended article: Short proofs are narrow -- resolution made simple
Recommended article: Short proofs are narrow—resolution made simple
Recommended article: Q3043797
Recommended article: Simplified and improved separations between regular and general resolution by lifting
Recommended article: Optimality of size-width tradeoffs for resolution
description: scientific article; zbMATH DE number 3939322