Sciweavers

SIAMCOMP
2000

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

13 years 3 months ago
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
Maria Luisa Bonet, Juan Luis Esteban, Nicola Gales
Added 19 Dec 2010
Updated 19 Dec 2010
Type Journal
Year 2000
Where SIAMCOMP
Authors Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, Jan Johannsen
Comments (0)