VSIDS

VSIDS (Variable State Independent Decaying Sum) is the heuristic by which CDCL solvers choose the variable to branch on^[1]. Every variable carries an activity score. When the solver analyzes a conflict, it bumps the activity of the variables involved, and all activities decay slowly as further conflicts occur, so that the score measures how often, and how recently, a variable has taken part in conflicts. Each decision picks the unassigned variable with the highest activity. The name records the two properties that made it successful: the score is independent of the variable state, the current assignment, so it costs nothing to maintain during propagation and backtracking, and it is a decaying sum that favours recent conflicts. The Chaff solver introduced VSIDS in 2001^[1], and MiniSat's variant^[2] is used in most solvers today.

Let $a_v$ be the activity of variable $v$ and $g$ a global increment, initially 1. After the $t$-th conflict, each variable that appears in a clause used by conflict analysis is bumped, and the increment grows by a constant factor^[2]:

Increasing the increment has the same effect as multiplying every score by $\rho$, without touching them. Relative to the current increment, the activity is an exponential moving average of the variable's participation in conflicts,

so a bump from $j$ conflicts ago counts ${\rho }^j$ as much as a fresh one. MiniSat uses $\rho =0.95$, a half-life of about 14 conflicts, and rescales all scores when they exceed $10^{100}$ to avoid overflow^[2]. Chaff's original version bumped the literals of each learned clause and periodically halved all counters^[1]. The unassigned variable of highest activity is found with a binary heap, which only needs updating when a score changes or a variable is unassigned.

(* Record the activity scores, divided by the current increment so that
   a score of 1 means "bumped just now", every 50 conflicts. *)
let colouring ~vertices ~edges ~colours =
  let x v c = (v * colours) + c + 1 in
  Cnf.of_clauses
    (List.init vertices (fun v -> List.init colours (x v))
     @ List.concat_map (fun (u, v) -> List.init colours (fun c -> [ - (x u c); - (x v c) ])) edges)
let random_graph n m =
  let rec go acc = if List.length acc = m then acc else
      let u = Random.int n and v = Random.int n in
      if u = v || List.mem (min u v, max u v) acc then go acc else go ((min u v, max u v) :: acc) in
  go []

conflict  x214 (late burst)  x144 (busy early)
     250        0.857        8.903
     500        0.000        8.337
     750        0.003       10.062
    1000        0.784       16.212
    1250        0.001       13.115
    1500        0.000        9.417
    1750        0.000       13.392
    2000        1.006       15.443
    2250        0.000       14.051
    2500        0.666        9.619
    2750        0.032       10.095
    3000        0.011        0.000

(* The same CDCL solver with VSIDS and with a fixed variable order. *)
let colouring ~vertices ~edges ~colours =
  let x v c = (v * colours) + c + 1 in
  Cnf.of_clauses
    (List.init vertices (fun v -> List.init colours (x v))
     @ List.concat_map (fun (u, v) -> List.init colours (fun c -> [ - (x u c); - (x v c) ])) edges)
 
let random_graph n m =
  let rec go acc = if List.length acc = m then acc else
      let u = Random.int n and v = Random.int n in
      if u = v || List.mem (min u v, max u v) acc then go acc else go ((min u v, max u v) :: acc) in
  go []

instance                   result  VSIDS conflicts      fixed order
random 3-SAT, 100 vars     UNSAT               420             2281
random 3-SAT, 120 vars     UNSAT               645             3624
pigeonhole, 8 in 7         UNSAT              4164              322
4-colouring, 60 vertices   UNSAT               535             2565
4-colouring, 70 vertices   UNSAT              3062            27192

On random and graph-colouring formulas, VSIDS needs between four and nine times fewer conflicts. On the pigeonhole formula the fixed order is better, because it happens to follow the structure of the formula, pigeon by pigeon, while VSIDS spreads its attention over the symmetric variables. Heuristics are not uniformly better; VSIDS wins because on the large structured formulas that solvers are used for, it concentrates on a small set of variables that are closely related through recent conflicts.

Why it works so well has been studied empirically. Liang and co-authors found that VSIDS favours variables that bridge the communities of the formula's variable-incidence graph, and that the variables it picks are strongly correlated with those that will appear in future conflicts^[4]. Because decisions follow conflicts, the search tends to stay in one region of the formula until it has learned what it needs there, which suits the locality of learned clauses.

VSIDS chooses a variable, not a value. Most solvers use phase saving: a variable is assigned the value it had when it was last unassigned^[6]. Combined with restarts, which undo all decisions but keep the activities and the saved phases, this lets the solver rebuild much the same assignment in a new variable order, and restarts become cheap enough to be frequent.

Before VSIDS, DPLL solvers chose variables by static counts over the current formula, such as the Jeroslow–Wang weights^[9], which must be recomputed as the formula changes and do not use conflicts at all. BerkMin bumped all clauses involved in a conflict and restricted decisions to the variables of the most recent learned clause that is not yet satisfied^[8]. VMTF, variable move-to-front, keeps the variables in a list and moves the bumped ones to the front, which gives similar behaviour with simpler data structures^[7]; Biere and Fröhlich compared it with the VSIDS variants and found them close^[3]. The learning-rate branching heuristic LRB treats the choice as a reinforcement-learning problem and rewards variables in proportion to how often they appear in learned clauses while assigned^[5]. Modern solvers often switch between VSIDS and one of these alternatives during a run.

Chaff, developed at Princeton by Moskewicz, Madigan, Zhao, Zhang and Malik and published in 2001, introduced VSIDS together with watched literals; the combination made it one to two orders of magnitude faster than the solvers before it on industrial benchmarks^[1]. BerkMin refined the idea in 2002^[8], and MiniSat's exponential version of 2003, which bumps variables during conflict analysis and grows the increment, became the standard^[2]. Phase saving was added in 2007^[6], and the heuristic has since been analyzed and challenged by VMTF and LRB^[3][5].

• CDCLConflict-driven clause learning (CDCL) is the algorithm of modern SAT solvers. It extends DPLL backtracking search with three ideas: when propagation falsifies a clause, conflict analysis derives a new clause that explains the conflict and adds it to the formula; the solver then backjumps non-chronologically to the decision level at which the new clause forces a literal; and branching follows the variables involved in recent conflicts. With watched literals, restarts and clause deletion, CDCL solvers decide industrial formulas with millions of variables, and with restarts they are as strong as general resolution, exponentially stronger than DPLL.
• First-UIP conflict analysisConflict analysis is the step of a CDCL SAT solver that explains a conflict by a new clause. Starting from the clause that became false, the solver repeatedly resolves it with the reason clauses of literals assigned at the current decision level, in reverse order of assignment, until only one literal of that level remains. That literal is the first unique implication point (UIP), a node through which every path from the decision to the conflict passes in the implication graph. The resulting clause is learned; it is implied by the formula, it forbids the combination of assignments that caused the conflict, and after backjumping to the second-highest level in it, it immediately propagates the negation of the UIP.
• Watched literalsThe two-watched-literal scheme is the data structure SAT solvers use to detect unit and conflicting clauses. Each clause of two or more literals watches two of its literals that are not false; a clause is examined only when one of its watched literals becomes false, and then it either finds a replacement watch, becomes unit, or is a conflict. Because the watches remain valid when assignments are undone, backtracking costs nothing, and a clause with many literals is touched only when its watches are hit. Introduced by the Chaff solver in 2001, it made unit propagation, which dominates solver time, several times faster.
• DPLLDPLL, the Davis–Putnam–Logemann–Loveland procedure, is the backtracking search algorithm for Boolean satisfiability on which all complete SAT solvers are built. It repeatedly simplifies a CNF formula by unit propagation and pure literal elimination, then chooses an unassigned variable and tries both of its values in turn, backtracking to the most recent choice when a clause becomes false. It is sound and complete, uses memory linear in the formula, and its runs on unsatisfiable formulas correspond to tree-like resolution proofs, which gives exponential lower bounds such as the n! − 1 decisions it needs for the pigeonhole formulas. Clause learning turned it into CDCL.
• Unit propagationUnit propagation is the inference rule at the core of SAT solvers: when every literal of a clause is false under the current partial assignment except one unassigned literal, that literal must be true. Applying the rule until nothing changes either extends the assignment or finds a clause with every literal false, a conflict. It decides satisfiability of Horn formulas on its own, it takes most of the running time of a modern CDCL solver, and it is implemented with two watched literals per clause so that only clauses that may have become unit are ever inspected.

1. [1]M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, “Chaff: engineering an efficient SAT solver”, DAC (2001).
2. [2]N. Eén, N. Sörensson, “An extensible SAT-solver”, SAT, Lecture Notes in Computer Science 2919 (2004).
3. [3]A. Biere, A. Fröhlich, “Evaluating CDCL variable scoring schemes”, SAT, Lecture Notes in Computer Science 9340 (2015).
4. [4]J. H. Liang, V. Ganesh, E. Zulkoski, A. Zaman, K. Czarnecki, “Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers”, Haifa Verification Conference (2015).
5. [5]J. H. Liang, V. Ganesh, P. Poupart, K. Czarnecki, “Learning rate based branching heuristic for SAT solvers”, SAT, Lecture Notes in Computer Science 9710 (2016).
6. [6]K. Pipatsrisawat, A. Darwiche, “A lightweight component caching scheme for satisfiability solvers”, SAT, Lecture Notes in Computer Science 4501 (2007).
7. [7]L. Ryan, Efficient Algorithms for Clause-Learning SAT Solvers, MSc thesis, Simon Fraser University (2004).
8. [8]E. Goldberg, Y. Novikov, “BerkMin: a fast and robust SAT-solver”, DATE (2002).
9. [9]R. G. Jeroslow, J. Wang, “Solving propositional satisfiability problems”, Annals of Mathematics and Artificial Intelligence 1 (1990).

last updated 28 September 2026