Regular Resolution Versus Unrestricted Resolution

Abstract

A resolution proof of an unsatisfiable propositional formula is called regular if and only if no variable is eliminated (with the resolution rule) twice on any branch of the proof tree representing the resolution proof. An infinite family of unsatisfiable propositional formulas is constructed and the following shown: These formulas have polynomial size unrestricted resolution proofs, whereas all regular resolution proofs of these formulas are of superpolynomial length.