Conflict-Driven Clause Learning

sat-solving logic

Definition

Conflict-Driven Clause Learning

Conflict-driven clause learning is a complete algorithm for the satisfiability problem that extends the DPLL algorithm by analysing conflicts and adding new clauses implied by the current formula. Whenever a partial assignment produces a conflict under unit propagation, the solver derives a learned clause that prevents the same conflicting assignment pattern from being repeated, then backtracks non-chronologically to a decision level at which the learned clause becomes unit.

Mechanism

Decision Phase (Branching): The solver selects an unassigned variable and assigns a truth value according to a branching heuristic. This creates a new decision level in the search tree.

Propagation Phase (Implication): After each decision, the solver applies unit propagation until no unit clause remains or a conflict is detected. The propagated assignments can be represented by an implication graph.

Conflict Analysis (Learning): If propagation derives the empty clause, the solver analyses the implication graph and derives a clause implied by the formula. This learned clause cuts off the current conflicting region of the search space.

Backjumping (Non-Chronological): Instead of undoing only the most recent decision, the solver jumps back to the highest decision level compatible with the learned clause. The learned clause is then typically unit and immediately propagates.

Restart Strategy (Global Search Control): Modern CDCL solvers often restart the search while retaining learned clauses. This combines global exploration with the accumulated information obtained from previous conflicts.

Properties

Correctness (Soundness and Completeness): Every learned clause is logically implied by the original formula, so learning preserves satisfiability. Since the procedure explores assignments together with learned constraints, CDCL remains complete.

Practical Strength (Clause Reuse): The central advantage of CDCL over plain DPLL is that conflicts are turned into reusable information. In practice, this dramatically reduces repeated exploration of equivalent failing assignments.

Example

Consider

$$F=c_1\wedge c_2\wedge c_3\wedge c_4\wedge c_5\wedge c_6$$

with

$$\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}$$

Propagation Sequence (Decision Levels): Suppose the solver makes the decisions $h=\top$ at level $1$, $b=\top$ at level $2$, an irrelevant decision $y=\top$ at level $3$, and $a=\top$ at level $4$. After substituting these assignments into $F$, the residual formula is

$$(c)\wedge (d)\wedge (\neg c\vee \neg d\vee e)\wedge (\neg e\vee f)\wedge (\neg e\vee g)\wedge (\neg f\vee \neg g).$$

Hence unit propagation proceeds as follows:

$$\begin{array}{rl}{F}_0& =(c)\wedge (d)\wedge (\neg c\vee \neg d\vee e)\wedge (\neg e\vee f)\wedge (\neg e\vee g)\wedge (\neg f\vee \neg g),\\ F_1& =(d)\wedge (\cancel{\neg c}\vee \neg d\vee e)\wedge (\neg e\vee f)\wedge (\neg e\vee g)\wedge (\neg f\vee \neg g),\\ F_2& =(e)\wedge (\neg e\vee f)\wedge (\neg e\vee g)\wedge (\neg f\vee \neg g),\\ F_3& =(f)\wedge (g)\wedge (\neg f\vee \neg g),\\ F_4& =(g)\wedge (\cancel{\neg f}\vee \neg g),\\ F_5& =(\neg g)\wedge (g).\end{array}$$

Thus propagation derives $c$, then $d$, then $e$, then $f$ and $g$, and finally the contradictory pair $(g)$ and $(\neg g)$. Equivalently, clause $c_6$ becomes unsatisfied, so a conflict is reached.

Learned Clause (Conflict Analysis): The conflict depends on the assignments $h$, $b$, and $a$. Hence one possible learned clause is

$$(\neg h\vee \neg b\vee \neg a).$$

This clause excludes the same conflicting combination in future search. Depending on the concrete learning scheme, a different but implied learned clause may be derived.

After learning $(\neg h\vee \neg b\vee \neg a)$, the solver backtracks to a decision level at which this clause is not yet falsified. The clause states that the assignments $h=\top$, $b=\top$, and $a=\top$ cannot simultaneously hold. Hence any future assignment must satisfy at least one of $\neg h$, $\neg b$, or $\neg a$, meaning that at least one of $h$, $b$, or $a$ must be set to $\perp$. In this way, the learned clause prevents the solver from revisiting the same conflicting configuration.