The size of the cache in which the lemmas are stored is fixed
throughout the branching process. The memory needed to maintain the
cache is automatically allocated and accomodates all lemmas in the
cache. Usually, the bigger the memory cache, the slower the search
process. Therefore one is confronted with the following optimization
problem: choose the lemma cache size small enough to avoid burdensome
overhead yet large enough that lemmas in the cache will significantly
reduce search. The parameter to use for controlling the lemma cache
is -max-cached-lemmas or -L and an example of its
use is this:
$ sbsat -L 1000 problem.cnf
It is possible to set the lemma cache to 0. This will prevent any lemma from being created.8 For example, use
$ sbsat -L 0 slider_80_unsat.ite
For some problems this will yield significantly better results than when the lemmas are used. See Section for a discussion of when to use lemmas and when not to use lemmas.
Remark: The heuristic used to discard lemmas from the cache when newly created lemmas are added to a full cache is not compatible with the option that disables lemma creation. Also the effectivness of the lemma heuristic decreases with descreasing lemma cache size. See Section for a discussion.
Remark: The Chaff-like (VSIDS) heuristic requires lemma creation and therefore is not compatible with the option that causes the lemmas not to be created (-L 0).
Backjumping is inherently tied to lemmas and therefore, the backjumping feature is active when -L has an argument greater than 0, and the backjumping feature is inactive when -L 0 is used. To turn the backjumping feature on, but store `almost' no lemmas, use the flag -L 1. Please consider the -backjumping flag deprecated.