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
Cutting Planes and resolution; in both cases 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  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 refutation provided to give the upper bound respects the stronger restriction of being a Davis-Putnam resolution proof. This extends the corresponding superpolynomial separation of . Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known .
CitationBonet, M., Esteban, J., Galesi, N, Johannsen, J. . "Exponential separation between tree-like and dag-like Cutting Planes proof systems". 1997.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: firstname.lastname@example.org