# Clarification on “clause learning” in DPLL algorithm

I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not already contain it, neither any subset of it). Here is what Knuth in his book says:

A conflict clause $$c$$ on decision level $$d$$ has the form $$\overline{l} \lor \overline{a}_1 \lor ··· \lor \overline{a}_k$$, where $$l$$ and all the $$a$$’s belong to the trail; furthermore $$l$$ and at least one $$a_i$$ belong to level $$d$$. We can assume that $$l$$ is rightmost in the trail, of all the literals in $$c$$. Hence $$l$$ cannot be the $$d$$th decision; and it has a reason, say $$l \lor \overline{a}′_1 \lor ··· \lor \overline{a}′_k$$. Resolving $$c$$ with this reason gives the clause $$c′ = \overline{a}_1 \lor ··· \lor \overline{a}_k \lor \overline{a}′_1 \lor ··· \lor \overline{a}′_k$$, which includes at least one literal belonging to level $$d$$. If more than one such literal is present, then $$c′$$ is itself a conflict clause; we can set $$c \leftarrow c′$$ and repeat the process. Eventually we are bound to obtain a new clause $$c′$$ of the form $$\overline{l}′ \lor \overline{b}_1 \lor ··· \lor \overline{b}_r$$, where $$l′$$ is on level $$d$$ and where $$b_1$$ through $$b_r$$ are on lower levels.

Such a $$c′$$ is learnable, as desired, because it can’t contain any existing clauses. (Every subclause of $$c′$$, including $$c′$$ itself, would otherwise have given us something to force at a lower level.)

I can understand why the clause database has no subset of $$c'$$ that contains $$\overline{l'}$$ (because $$\overline{l'}$$ would have been forced (i.e. unit-propagated) at level lower than $$d$$), but what contradicts to the existence of clause, let's say, $$\overline{b_1}\lor\overline{b_2}$$?

All the literals in a conflict clause are set false by definition, else there would be no conflict. So if the clause $$\overline{b_1}\lor\overline{b_2}$$ existed, one of those false literals would have caused that clause to go unit before we reached the current level, which in turn would have forced one of the $$\overline{b_1}$$ or $$\overline{b_2}$$ literals true. But we already know that those literals must be false, so we have a contradiction. This contradiction shows that the clause $$\overline{b_1}\lor\overline{b_2}$$ cannot exist. The reasoning is the same for all clauses that are subsets of the conflict clause.
• Thanks a lot, I think I've got it. If this subset contains $\overline{l'}$, then $\overline{l'}$ would be propagated at level $d'$ (but it was at level $d > d'$), if it does not, then we would have found a conflict at level $d'$ (but we did at $d > d'$). So, as far as I can see it is crucial for soundness to resolve until the conflict clause has the only literal from the last decision level. It is correct? I believe in other sources I have seen it mentioned as a heuristic and it confused me a lot. – Vladislav Feb 24 at 20:36