作者
Stephen Cook, Toniann Pitassi
发表日期
1990/3/16
期刊
Information Processing Letters
卷号
34
期号
2
页码范围
81-85
出版商
Elsevier
简介
Haken [4] first proved the intractability of resolution by showing that a family of propositional formulas encoding the pigeon-hole principle require superpolynomial-sized resolution proofs. Later, several authors [6, 1, 2] extended Haken’s techniques to obtain exponential lower bounds on the size of resolution proofs. All of these results are based on the counting method used by Haken and later reformulated as a probabilistic method by Urquhart 161.
In this paper we describe a simpler and more direct method which can replace the counting and probabilistic methods. Our method is feasibly constructive in the sense discussed in [3]. Informally, this means that all concepts in the proof are polynomial time. We present a polynomial time greedy algorithm which, when presented with a candidate resolution proof that is too short, produces a mistake in the proof. Further, we present a feasibly constructive correctness proof for the algorithm. In contrast, the counting arguments show the existence of the mistake indirectly by bounding the sizes of exponentially large sets. In [3] it is shown (Theorem 10.16) that an “extended Frege system”(a kind of propositional proof system stronger than resolution) cannot
引用总数
学术搜索中的文章
S Cook, T Pitassi - Information Processing Letters, 1990