In this video, Nagat, we will continue from last time where we had this idea that we would

find out what went wrong in one branch of a DPLL run and then transport this information as a

clause into the other branches to actually shortstop them and conserve a lot of work.

So, the example that motivated this was that if we take a good old input clause set that is

unsatisfying, but distract DPLL by this nasty clause, two clauses that have 100 variables each,

which actually, since it is handcrafted like this, actually chases DPLL into a large tree,

which has the same kind of resolution clause, empty clause here at the lower end. So, we have

a hundred situations, we have lots of branches that actually have the same form. The hope here

is that we can go through the first branch, learn a clause here, and not have to go into all of the

other branches, but go into the false case here, which actually will trigger the actual proof here.

So, again, if we want to learn, we need to figure out what went wrong and then learn information

that we will remember that will not actually let us do the same thing again. For DPLL, we have to

analyze why unit propagation yielded a conflict. In this section, we learn how to analyze the

conflicts and in the next section, we can actually make a clause out of this information.

We will, however, need some concepts here, which kind of fall down from the heavens,

but do exactly the right thing. So, we're going to look at branches in a DPLL

derivation, and then we will call a variable P on that branch. The choice literal

if its value is set by a splitting rule, and implied literal if it is set by a unit

propagation rule, and the conflict literal if it contributes to a derivation of the empty clause.

Not all of them do. From that, we can make an implication graph, which is just a

directed graph where the nodes are labeled with the choice and implied literals along B. Also,

we have a conflict vertex, which is an empty clause for every clause C that became empty

on that branch. So, those are the nodes or vertices. Now, we need some edges. If we have a clause

containing a literal L prime, which became unit with the implied literal L prime, meaning all of

the L1 to the LK actually went away on this branch, then we actually have edges from all the

opposite literals to the ones in this clause, namely the ones that were used to resolve those

away, if you will, until only L prime is left. We will have edges for all of those. And we need

edges into the conflict vertices. So, if I have a clause C that became empty and therefore gives me

one of these conflict vertices, we will just take all the opposites of the literals that were resolved

away in the process of making C empty and add those edges to the graph. Now, you can ask

yourselves, why are all these things here that are the starting points of the edges here?

Why are those already in the graph? Well, because these clauses became empty. So, we had to have,

had to set the value L1 to false, to L2 to false. So, they are actually choice or implied literals

in the graph already. We can also convince ourselves that it's acyclic that basically comes

from the order of things in the tree and the way we've defined the edges. Let me make an example

here. If we actually look at the vanilla 1 derivation again, so we remember that the

unit clause are true. So, we unit propagate R to true, which actually drops the Rs from the rest,

giving us this clause set. But now we basically record what the implied and choice literals are.

So, we have R true because we set R to true as an implied and we have R2 as an implied. So,

we have R true because we set R to true as an implied literal. So, this ends up in the branch.

So, we used the splitting rule again and remember that we had an A branch and a B branch in the

derivation. We're only interested in the A branch at the moment. So, we have split in this branch P

to false, which makes P false a choice literal and gives us Q true and Q false, the two clauses.

And in this case, we unit propagate in this case with Q and true. So, we get an implied literal

Q true. And since this became empty, we have edges R true, Q true and P false, Q true here.

And then since we end up with an empty literal, we have a conflict literal for P true and Q false,

which gives us two more edges. And if we collect all that information,

that gives me a graph that looks like this. The interesting fact here is if we look at

the redundancy one, which is essentially just, is very similar. And we have the nasty subtree here

and the other thing there, then you can see by the same reasoning, we end up with a graph,