3.2 Branching Sequence

We use the notion of branching sequence to prove an exponential separation between DPLL and clause learning. It generalizes the idea of a static variable order by letting the order differ from branch to branch in the underlying DPLL procedure. In addition, it also specifies which branch (TRUE or FALSE) to explore first. This can clearly be useful for satisfiable formulas, and can also help on unsatisfiable ones by making the algorithm learn useful clauses earlier in the process.

Definition 3   A branching sequence for a CNF formula F is a sequence $\sigma$ = (l₁, l₂,..., l_k) of literals of F, possibly with repetitions. A DPLL based algorithm $\mathcal {A}$ on F branches according to $\sigma$ if it always picks the next variable v to branch on in the literal order given by $\sigma$, skips v if v is currently assigned a value, and otherwise branches further by setting the chosen literal to FALSE and deleting it from $\sigma$. When $\sigma$ becomes empty, $\mathcal {A}$ reverts back to its default branching scheme.

Definition 4   A branching sequence $\sigma$ is complete for a formula F under a DPLL based algorithm $\mathcal {A}$ if $\mathcal {A}$ branching according to $\sigma$ terminates before or as soon as $\sigma$ becomes empty. Otherwise it is incomplete or approximate.

Clearly, how well a branching sequence works for a formula depends on the specifics of the clause learning algorithm used, such as its learning scheme and backtracking process. One needs to keep these in mind when generating the sequence. It is also important to note that while the size of a variable order is always the same as the number of variables in the formula, that of an effective branching sequence is typically much more. In fact, the size of a branching sequence complete for an unsatisfiable formula F is equal to the size of an unsatisfiability proof of F, and when F is satisfiable, it is proportional to the time needed to find a satisfying assignment.