VSIDS

also: activity heuristic, branching heuristic, decision heuristic

Variable State Independent Decaying Sum: the branching heuristic in every modern SAT solver. Each variable carries an activity score, conflict analysis bumps the ones it touches, and all scores decay, so the search concentrates on whatever part of the formula is currently producing conflicts.

Which variable to branch on next is the one genuinely heuristic choice in a SAT solver, and the one that decides whether an instance takes a second or a week. VSIDS answers it with a score per variable: bump the variables that conflict analysis touches, decay every score periodically, and always branch on the highest.

The effect is that the search concentrates on whatever part of the problem is currently producing conflicts, and drifts as that changes. It is a locality heuristic, not a measure of anything structural about the formula.

Decaying every score each conflict would be linear in the variable count. Inflating the bump instead is equivalent and constant time, with a rescale only when the floats are about to lose precision.

let bump (s : t) (v : int) =
  s.act.(v) <- s.act.(v) +. s.inc;
  if s.act.(v) > 1e100 then begin
    Array.iteri (fun i a -> s.act.(i) <- a *. 1e-100) s.act;
    s.inc <- s.inc *. 1e-100
  end
 
let decay_all (s : t) = s.inc <- s.inc /. s.decay

Three conflicts touching {x1,x2}, {x2,x3}, {x2,x5}. Compiled with ocamlopt 4.14.1.

x1 activity 1.0000
x2 activity 3.1607
x3 activity 1.0526
x4 activity 0.0000
x5 activity 1.1080
next decision: x2

x2 wins because it appeared in all three conflicts, and x5 edges out x3 because its conflict was more recent. That ordering, recency over raw frequency, is the whole point of the decay.