Hybrid Approaches

Finally, we note that some solvers employ a hybrid approach. The CHAFF algorithm [Moskewicz, Madigan, Zhao, Zhang, MalikMoskewicz et al.2001] uses both a relevance bound and a (larger) length bound. Clauses must meet both the relevance bound and the length bound to be retained.

Yet another approach is taken by the BERKMIN algorithm [Goldberg NovikovGoldberg Novikov2002]. Here, the set of nogoods is partitioned into two separate groups based on how recently the nogoods were acquired; $\frac{15}{16}$ of the nogoods are kept in a ``recent'' group and the remaining $\frac{1}{16}$ in an ``old'' group. A relatively large length bound is used to cull the recently acquired nogoods while a smaller length bound is used to aggressively cull the smaller group of older nogoods. We are not aware of any studies comparing these hybrid approaches to pure length-bounded or relevance-bounded methods.