3
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Vladislav Feb 24 at 20:36
  • $\begingroup$ It is a heuristic; continuing to resolve isn't necessary for soundness. The solver could learn the clause produced from resolving the first conflict clause and the conflict literal's reason, or it could continue resolving until there's only one literal from the current level and learn that clause. The latter produces greater backjump distances; that's the main reason to do it. $\endgroup$ – Kyle Jones Feb 25 at 1:52
  • $\begingroup$ But in that case (when it might be more than one literal from the last decision level) the proof presented is not relevant, is it? $\endgroup$ – Vladislav Feb 27 at 12:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.