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. © 2010 Springer-Verlag.
CITATION STYLE
Ben-Sasson, E., & Johannsen, J. (2010). Lower bounds for width-restricted clause learning on small width formulas. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6175 LNCS, pp. 16–29). https://doi.org/10.1007/978-3-642-14186-7_4
Mendeley helps you to discover research relevant for your work.