Module varisat::decision::vsids

The VSIDS branching heuristic.

The VSIDS (Variable State Independent Decaying Sum) branching heuristic keeps an activity value for each variable. For each conflict some variables are bumped, which means that their activity is increased by a constant. After bumping some variables, the activity of all variables is decayed by multiplying it with a constant below 1.

When a decision is made, it branches on the vairable with the highest activity among the unassigned variables.

There are a few variants that differ in which variables are bumped. Varisat follows Minisat (and others) by bumping all variables in the conflict clause and all variables resolved on during conflict analysis.

Structs

Vsids

The VSIDS branching heuristic.