next up previous contents
Next: The lemma cache Up: Quick Start - Some Previous: Preprocessor command   Contents

Heuristics

Two search heuristics are included with SBSAT. One of these we refer to as the LSGB heuristic for Locally Skewed, Globally Balanced. It is designed to work well on inputs with little (known) structure and therefore favors assignments that reveal inferences which can be derived from information about individual functions (locally skewed) and simultaneously favors assignments that tend to balance the entire search space (globally balanced). For more information on this heuristic and insights for its control see Section [*].

The other search heuristic is a variant of the VSIDS heuristic Chaff uses. See Section [*] for information about the use and control of this heuristic.

There is also an option, which we call combined, that allows the user to mix the two heuristics. What this mixing accomplishes is given in Section [*].

The following table shows command line switches for selecting these heuristics and associated parameters.

Heuristic Default Switch Description
LSGB yes -H j Locally Skewed, Globally Balanced
VSIDS no -H l Number of occurrences of literals
Combined no -H jl Combination of the two above


next up previous contents
Next: The lemma cache Up: Quick Start - Some Previous: Preprocessor command   Contents
John Franco 2011-09-15