Exponential separation between tree-like and dag-like Cutting Planes proof systems
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/83891
Tipus de documentReport de recerca
Data publicació1997-12
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
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 [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 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 [30]. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known [14].
CitacióBonet, M., Esteban, J., Galesi, N, Johannsen, J. . "Exponential separation between tree-like and dag-like Cutting Planes proof systems". 1997.
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
Exponential_sep.pdf | 177,1Kb | Visualitza/Obre |