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 ... more >>>