I am trying to understand how Conflict-Driven Clause Learning works. After reading through the lecture slides, wikipedia article and some additional slides I found online I realized that I still can't understand CDCL enough to do the assignment.
I find very hard to follow the examples online since all of them differ in notation and lack simple description of why and what is going on. Why do we choose exactly literal A or B, what is the result of unit propagation and how it affects our next steps? How do we choose what to save in the implication graph? All in all, I just need 2, 3 simple examples that illustrate the process in detail.
Let's take wikipedia example step 2. Why are we choosing x4 to be the vertex in our implication graph? Is it because it is the only literal left from unit propagation or just because we decide so? This, not explained.
Next, step 3. Why is x3 chosen? Wiki says it's arbitrary? This is not a good explanation.
Next, step 4. Why x1 point to x8 as well as x3? No answer to that.
I can continue but I feel like it makes no sense since I don't understand the beginning.
I'm not very familiar, at this point in time, with this topic, but I can make out enough to guess at answers your questions.
"Let's take wikipedia example step 2. Why are we choosing x4 to be the vertex in our implication graph? Is it because it is the only literal left from unit propagation or just because we decide so? This, not explained. "
We start the problem with the assumption that all of the clauses are true. It says:
"The satisfiability problem consists in finding a satisfying assignment for a given formula in conjunctive normal form (CNF)."
A satisfying assignment is an assignment of truth values to the variables such that all clauses hold as true.
So, in step 1, we select some branching variable and assume it's false. In the example in the Wikipedia example we have x1 selected in the clause:
x1 + x4.
But x1 + x4. is True by assumption. Thus, since x1 = False, we know that
False + x4 = True.
Since x4 is either True or False, if x4 = False, then we would have:
False + False = True.
But since "+" is logical disjunction and for all x, x + x = x, we would have
False = True.
A contradiction. Therefore, x4 = True. Can we infer the truth value of any other literal in the clauses? Nope (or at least not so easily). Therefore, it stands to reason that x4 is selected, because we can infer it as true immediately. Note also that in step 2 we have x4 = 1.
"Next, step 3. Why is x3 chosen? Wiki says it's arbitrary? This is not a good explanation."
x3 is the first variable in the sequence of clauses which we don't know the truth value of yet. Also, at this step in the algorithm, there's no other values of variables that we can determine.
** Next, step 4. Why x1 point to x8 as well as x3? No answer to that. **
In step 2 we have x1 = 0 pointing to x4 = 1. This is equivalent to saying "if x1 is False, then x4 is True." This is consistent with the clause x1 + x4 holding as True, or equivalently x1 + x4 = True.
Similarly, in step 4 we could read the new information as saying:
"If x1 is False and x4 is True, then x8 is False."
That is consistent with x1 + x3 + x8' = True.