期刊名称:Electronic Colloquium on Computational Complexity
印刷版ISSN:1433-8092
出版年度:2010
卷号:2010
出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要: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 resolution width lower bounds. This yields the first lower bounds on width-restricted clause learning for formulas in 3-CNF.