查看文章

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