We prove an exponential lower bound for tree-like Cut- ting Planes refutations of a set of clauses which has polyno- mial 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 superpoly- nomial separations were known before [30, 20, 10]. In or- der 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 refu- tation 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].

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems / BONET M., L; Esteban, J. L.; Galesi, Nicola; Johannsen, J.. - STAMPA. - 39:(1998), pp. 638-647. (Intervento presentato al convegno 39th Annual Symposium on Foundations of Computer Science, FOCS '98, tenutosi a Palo Alto, California, USA.) [10.1109/SFCS.1998.743514].

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

GALESI, NICOLA
;
1998

Abstract

We prove an exponential lower bound for tree-like Cut- ting Planes refutations of a set of clauses which has polyno- mial 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 superpoly- nomial separations were known before [30, 20, 10]. In or- der 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 refu- tation 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].
1998
39th Annual Symposium on Foundations of Computer Science, FOCS '98,
Resolution Cutting Planes, real communication complexity
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems / BONET M., L; Esteban, J. L.; Galesi, Nicola; Johannsen, J.. - STAMPA. - 39:(1998), pp. 638-647. (Intervento presentato al convegno 39th Annual Symposium on Foundations of Computer Science, FOCS '98, tenutosi a Palo Alto, California, USA.) [10.1109/SFCS.1998.743514].
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/205918
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 17
social impact