All reports by Author Jan Johannsen:

__
TR13-072
| 3rd May 2013
__

Jan Johannsen#### Exponential Separations in a Hierarchy of Clause Learning Proof Systems

__
TR10-085
| 20th May 2010
__

Eli Ben-Sasson, Jan Johannsen#### Lower bounds for width-restricted clause learning on small width formulas

__
TR01-056
| 6th August 2001
__

Michael Alekhnovich, Jan Johannsen, Alasdair Urquhart#### An Exponential Separation between Regular and General Resolution

__
TR98-035
| 8th May 1998
__

Maria Luisa Bonet, Juan Luis Esteban, Jan Johannsen#### Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

__
TR97-032
| 11th July 1997
__

Jan Johannsen#### Lower Bounds for Monotone Real Circuit Depth and Formula Size and Tree-like Cutting Planes

Jan Johannsen

Resolution trees with lemmas ($\mathrm{RTL}$) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments $\mathrm{RTL}(k)$ are related to clause learning algorithms where the width of learned clauses is bounded by $k$.

For every $k$ up to $O(\log n)$, an exponential separation ... more >>>

Eli Ben-Sasson, Jan Johannsen

It has been observed empirically that clause learning does not significantly improve the performance of a SAT solver when restricted

to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from ...
more >>>

Michael Alekhnovich, Jan Johannsen, Alasdair Urquhart

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.

Maria Luisa Bonet, Juan Luis Esteban, Jan Johannsen

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

Jan Johannsen

Using a notion of real communication complexity recently

introduced by J. Krajicek, we prove a lower bound on the depth of

monotone real circuits and the size of monotone real formulas for

st-connectivity. This implies a super-polynomial speed-up of dag-like

over tree-like Cutting Planes proofs.