Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR13-072 | 3rd May 2013 16:55

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

TR13-072
Authors: Jan Johannsen
Publication: 13th May 2013 08:23
Downloads: 2355
Keywords:

Abstract:

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 between the proof systems $\mathrm{RTL}(k)$ and $\mathrm{RTL}(k+1)$ is shown.

ISSN 1433-8092 | Imprint