Width versus size in resolution proofs

摘要

A general theme in the proof of lower bounds on the size of resolution refutations in propositional logic has been that of basing size lower bounds on lower bounds on the width of refutations. Ben-Sasson and Wigderson have proved a general width-size tradeoff result that can be used to prove many of the lower bounds on resolution complexity in a uniform manner. However, it does not apply directly to the well known pigeonhole clauses. The present paper generalizes their width-size tradeoff so that it applies directly to (a monotone transformation of) the pigeonhole clauses. (c) 2007 Elsevier B.V. All rights reserved.