Loading jsMath...
Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR13-072 | 3rd May 2013 16:55

Exponential Separations in a Hierarchy of Clause Learning Proof Systems

RSS-Feed




TR13-072
Authors: Jan Johannsen
Publication: 13th May 2013 08:23
Downloads: 4839
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