Conflict-Driven Clause Learning

Definition

Conflict-Driven Clause Learning

Let $F$ be a CNF formula and let $M$ be a trail of decisions and propagated literals. Conflict-driven clause learning (CDCL) extends the DPLL algorithm as follows: when unit propagation falsifies a clause, the solver resolves that conflict clause with the reason clauses recorded in $M$ to derive a learned clause $L$ satisfying

$$F\models L.$$

It adds $L$ to $F$ and backtracks directly to a decision level at which $L$ becomes unit. The conflict therefore becomes a reusable constraint rather than a failed branch that may be explored again.

Mechanism

CDCL repeats the cycle

$$\text{decide}⟶\text{propagate}⟶\text{conflict}⟶\text{learn}⟶\text{backjump}.$$

CDCL cycle

1. Decide: assign an unassigned variable and begin a new decision level.
2. Propagate: apply unit propagation and record the reason clause for every forced literal.
3. Analyse: when a clause becomes false, resolve it with reason clauses to obtain a learned clause.
4. Backjump: undo assignments to the highest earlier level occurring in the learned clause; the clause then propagates immediately.

A conflict at decision level $0$ proves unsatisfiability. If every variable is assigned without conflict, the trail is a satisfying assignment.

Correctness

Every learned clause is obtained by resolution, so adding it preserves the models of $F$:

$$F\models L⟹\mathrm{Mod}(F)=\mathrm{Mod}(F\wedge L).$$

CDCL remains complete, but avoids repeating conflicts. Restarts may discard the current trail while retaining learned clauses, so earlier conflicts continue to constrain later search.

Example

Propagation reaches a conflict

Consider

$$\begin{array}{rlrl}{c}_1& =(\neg a\vee \neg b\vee c),& c_2& =(\neg a\vee d),\\ c_3& =(\neg c\vee \neg d\vee e),& c_4& =(\neg h\vee \neg e\vee f),\\ c_5& =(\neg e\vee g),& c_6& =(\neg f\vee \neg g).\end{array}$$

Suppose the solver decides

$$h=\top (1),b=\top (2),a=\top (3),$$

where parentheses indicate decision levels. Unit propagation gives

$$\begin{array}{rlrl}{c}_1& ⟹c=\top ,& c_2& ⟹d=\top ,\\ c_3& ⟹e=\top ,& c_4& ⟹f=\top ,\\ c_5& ⟹g=\top ,& c_6& =(\neg f\vee \neg g)=\perp .\end{array}$$

Thus $c_6$ is the conflict clause.

The implication graph records which clause forced each assignment. The highlighted assignment $e$ is the first unique implication point: every path from the current decision $a$ to the conflict passes through it.

Resolve $c_6$ first with the reason for $f$, then with the reason for $g$:

$$\begin{array}{rl}(\neg f\vee \neg g)& \stackrel{c_4}{\Rightarrow }(\neg g\vee \neg h\vee \neg e)\\ & \stackrel{c_5}{\Rightarrow }(\neg h\vee \neg e).\end{array}$$

The learned first-UIP clause is therefore

$$L=(\neg h\vee \neg e).$$

Only $e$ belongs to the current level. CDCL backjumps from level $3$ to level $1$, where $h=\top$ makes $L$ unit and forces $e=\perp$.

If resolution continues to the decisions, it instead yields

$$\begin{array}{rl}\neg h\vee \neg e& \stackrel{c_3}{\Rightarrow }\neg h\vee \neg c\vee \neg d\\ & \stackrel{c_2,c_1}{\Rightarrow }\neg h\vee \neg a\vee \neg b.\end{array}$$

This clause states that $h=\top$, $a=\top$, and $b=\top$ cannot hold simultaneously. Both clauses are consequences of $F$; modern solvers usually stop at the first UIP.