文章基本信息
- 标题：Exponential Separations in a Hierarchy of Clause Learning Proof Systems
- 本地全文：下载
- 作者：Jan Johannsen
- 期刊名称：Electronic Colloquium on Computational Complexity
- 印刷版ISSN：1433-8092
- 出版年度：2013
- 卷号：2013
- 出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
- 摘要：
Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments RTL(k) are related to clause learning algorithms where the width of learned clauses is bounded by k.
- 关键词：resolution; clause learning
