TAOCP 7.2.2.2 Exercise 266
In step C6, Algorithm C reaches a decision point when unit propagation has ended without producing a contradiction.
Section 7.2.2.2: Satisfiability
Exercise 266. [20] In order to keep from getting into a rut, CDCL solvers are often designed to make decisions at random, with a small probability $p$ (say $p = .02$), instead of always choosing a variable of maximum activity. How would this policy change step C6?
Verified: no
Solve time: 2m56s
Solution
In step C6, Algorithm C reaches a decision point when unit propagation has ended without producing a contradiction. The original rule chooses an unassigned variable of largest activity and assigns a value to it. The proposed randomization changes only this choice of the branching variable; all subsequent CDCL operations remain unchanged.
Let $U$ denote the set of variables that are currently unassigned at step C6. The modified step C6 first generates a random event whose probability of success is $p$. If this event succeeds, C6 chooses a variable $v\in U$ uniformly at random. If the event fails, C6 uses the original activity heuristic and chooses a variable $v\in U$ whose activity is maximum.
Therefore the modified variable-selection rule is
$$ v\leftarrow \begin{cases} \text{a uniformly chosen element of }U, & \text{with probability }p,\[4pt] \text{an element of }U\text{ having maximum activity}, & \text{with probability }1-p . \end{cases} $$
After $v$ has been chosen, the remainder of C6 is unchanged. The selected variable receives the chosen decision value, the new decision level is created, and the assignment is inserted into the implication trail exactly as in the original algorithm. The watched-literal structures and the clause database are not modified by this policy, because they depend on the assignments produced by C6 and not on the method used to select the decision variable.
For the suggested value $p=.02$, the maximum-activity heuristic is applied with probability
$$ 1-p=1-.02=.98, $$
and the random choice is applied with probability $.02$. Hence step C6 becomes a randomized branching rule while preserving every invariant required by the later propagation and conflict-analysis steps.
$$ \boxed{\text{Step C6 chooses a random unassigned variable with probability }p\text{ and otherwise chooses the maximum-activity variable.}} $$