On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems

An exponential lower bound for the size of tree-like cutting planes refutations of a certain family of conjunctive normal form (CNF) formulas with polynomial size resolution refutations is proved. This implies an exponential separation between the tree-like versions and the dag-like versions of resolution and cutting planes. In both cases only superpolynomial separations were known [A. Urquhart, Bull. Symbolic Logic, 1 (1995), pp. 425

• Type: Journal
• Year: 2000
• Where: SIAMCOMP
• Authors: Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, Jan Johannsen
• Keywords: Exponential Separation, Lower Bounds, SIAMCOMP 2000, Superpolynomial Separation