VSIDS

VSIDS, or Variable State Independent Decaying Sum, is a dynamic variable ordering heuristic used in modern SAT solvers, particularly those based on conflict-driven clause learning (CDCL). It guides the choice of which unassigned variable to branch on next, in order to prune the search space efficiently.

Implementation associates an activity score with each variable. When a conflict is derived and a clause is learned, the variables appearing in that clause have their activities increased (bumped). Periodically, all activities are multiplied by a decay factor less than one, so recent conflicts dominate. The next decision variable is chosen as the unassigned variable with the highest activity. Polarity is usually ignored in the primary score, and tie-breaks rely on secondary heuristics such as recency or variable order.

VSIDS has had a major influence on SAT solvers. It is lightweight, interpretable, and adapts to problem structure during search, especially under restarts. Over time, variants and refinements have tuned bump and decay constants and integrated VSIDS with other metrics (for example, LBD-based criteria) to improve performance across diverse benchmarks.