next up previous contents
Next: Controlling preprocessing and search Up: Quick Start - Some Previous: Heuristics   Contents

The lemma cache

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.


next up previous contents
Next: Controlling preprocessing and search Up: Quick Start - Some Previous: Heuristics   Contents
John Franco 2011-09-15