Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > REGULAR RESOLUTION:
Reports tagged with regular 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 >>>

TR01-056 | 6th August 2001
Michael Alekhnovich, Jan Johannsen, Alasdair Urquhart

#### An Exponential Separation between Regular and General Resolution

This paper gives two distinct proofs of an exponential separation
between regular resolution and unrestricted resolution.
The previous best known separation between these systems was
quasi-polynomial.

more >>>

TR19-178 | 5th December 2019
Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov

#### Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs

We show that the size of any regular resolution refutation of Tseitin formula \$T(G,c)\$ based on a graph \$G\$ is at least \$2^{\Omega(tw(G)/\log n)}\$, where \$n\$ is the number of vertices in \$G\$ and \$tw(G)\$ is the treewidth of \$G\$. For constant degree graphs there is known upper bound \$2^{O(tw(G))}\$ ... 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