Hello, in this video nugget, we're going to study our DPLL procedure again, and we will

realize and in fact prove that DPLL is actually or can be seen as a restricted form of resolution.

So let's start why we might think this. So if you think about unit propagation, remember

real unit propagation looks for unit clauses, say p true, and then realizes that all clauses

must be satisfied. So the only way we can assign p in our assignment that we're building

up in the branch of DPLL is that we make actually p true, which means that all the p falses

in any other clauses must be unsatisfiable. So we can actually drop them from the clauses

and that is iterated in unit propagation until there are no more unit clauses. So we can

see that this is actually the same as a form of resolution. Say we have a unit clause p

beta, say true, then we can drop all the clauses, the opposite literals from the clauses by

just resolution. This is we resolve on p alpha and p beta, of course, whatever works with

true works with false. And that gives us the rest C because the rest of the right hand

clause is actually empty. So we can do use the resolution calculus in this special kind

of resolution, which we call unit resolution to simulate what unit propagation is doing.

We realize that unit resolution is sound. Of course, it's a special case of resolution,

which we know to be sound. And we can convince ourselves easily with this example here where

we have four clauses with two literals, namely all the combinations of p and q and true and

false, which in this way, of course, is unsatisfiable. But we cannot derive the empty clause with

unit resolution. Why? Because there are no units. So we can't make any progress towards

the empty clause. So we can think of unit propagation as a very limited, incomplete,

but sound resolution calculus. Now, the question is, can we do the same thing in general? And

indeed, we can prove this. We prove this by an induction actually on the number of decisions

that a DPL run does. And this number of decisions is all the number of times we set a truth

value by either unit propagation or splitting. Essentially, this kind of decisions the DPL

run does. So the theorem, the actual theorem we're going to prove is that if DPLL returns

unsatisfiable on an input set delta, then I can build, I can generate a resolution refutation

with a refutation whose length is at most the number of decisions in the DPLL run we're

looking at. How do we do this? Well, we can first consider DPLL without unit propagation.

Remember unit propagation is something we can already do, we can already simulate by

resolution. So if we have a leaf node of this DPLL run for a proposition X, where the truth

values directly result in a clause C that has become empty. Remember that some of the

clauses become empty, they kind of get whittled away by the whole process of splitting and

unit propagation. Then we can see whether X is false, then we have to have an X true

because that's what went away and duly if X is true, then in the assignment then the

respective clause must be having X false. So we can resolve those two clauses to a clause

we call C of N that does not contain X because all the X's went away. So if you look at it,

the C of N, because it's in this run tree in this branch, it can only have the negations

of decision literals from above this node. So we remove this leaf node from the tree

and then iterate the argument kind of rippling up all the leaves in this tree. Once that's

the case, we've derived the empty clause. Only splitting here, unit propagation you

can either do as said in the other slide or we can just simulate unit propagation by splitting.

How that works we're going to see in the next example. So we have our well-known example

vanilla two and we have a unit propagation run here where we propagate the S from the

input, the Q, the R and the P and we simulate all of those by splitting. We split against,

we split on F and that makes, if we make S false, that makes S true empty. Then we go

down the S true branch, we split on Q, that makes Q, if Q is false, that makes Q true

and S false empty because we are on true false here. And you can see that this again is one

of the input clauses that became empty at this place. And we go on and on and on and

so we have a tree that we've decorated via a splitting tree that we've decorated with

the input clauses. In this case, every input clause appears exactly once. In a general