// Search randomization will collect equivalent 'max valued' variables, and
// pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST,
// all unassigned variables are equivalent. If the variable strategy is
// CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned
// variables, then the set of max valued variables will be all unassigned
// variables where
// lm <= variable min <= lm + search_randomization_tolerance
As I understand it, if your search branching strategy is set to FIXED_SEARCH then search randomization causes the variable selection strategy to break ties randomly instead of using the order in which the variables were defined.
It's unclear what search randomization does when the branching strategy is kept to be the default (which uses the underlying SAT solver's heuristics to branch). Perhaps it simply randomizes the initial VSIDS activity values in the SAT solver?
Curtis