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 cutting planes and resolution; in both cases only superpolynomial separations were known before. In order to prove this, we extend the lower bounds on the depth of monotone circuits of R. Raz and P. McKenzie (1997) to monotone real circuits. In the case of resolution, we further improve this result by giving an exponential separation of tree-like resolution front (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Puatam resolution proof. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separations was previously known.