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.
|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|