Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with Davis-Putnam resolution:
TR98-035 | 8th May 1998
Maria Luisa Bonet, Juan Luis Esteban, Jan Johannsen

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 ... more >>>

TR20-105 | 14th July 2020
Zoë Bell

Automating Regular or Ordered Resolution is NP-Hard

We show that is hard to find regular or even ordered (also known as Davis-Putnam) Resolution proofs, extending the breakthrough result for general Resolution from Atserias and Müller to these restricted forms. Namely, regular and ordered Resolution are automatable if and only if P = NP. Specifically, for a CNF ... more >>>

ISSN 1433-8092 | Imprint