Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like proofs for both CuttingPlanes andresolution; in bothcases only superpolynomial separations were known before [30, 20, 10]. In order to prove this, we extend the lower bounds on the depth of monotone circuits of Raz and McKenzie [26] to monotone real circuits. In the case of resolution, we further improve this result by giving an exponential separation of tree-like resolution from (dag-like) regular resolution proofs. In fact, the refutationprovided togive the upper boundrespects the stronger restriction of being a Davis-Putnam resolution proof. This extends the corresponding superpolynomial separation of [30]. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously kno...

• Type: Conference
• Year: 1998
• Where: FOCS
• Authors: Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, Jan Johannsen
• Keywords: Exponential Separation, FOCS 1998, Resolution Proofs, Superpolynomial Separation, Theoretical Computer Science