Length-bounded Learning

The first method used to bound the size of the set of learned clauses was to only retain clauses whose length is less than a given bound $k$ [DechterDechter1990,Frost DechterFrost Dechter1994]. In addition to providing a polynomial bound on the number of nogoods retained, this approach was felt likely to retain the most important learned clauses, since a clause of length $l$ will in general prune $\frac{1}{2^l}$ of the possible assignments of values to variables. Length-bounded learning draws from this observation the conclusion that short clauses should be retained in preference to long ones.