Come on.

Essentially, we had two rules.

One is unit propagation,

which is essentially based on the idea that if you have a clause set,

we talked about this, clause sets are wonderful for implementation.

You can take sets of bit or lists of bit vectors or lists of lists of bits or those kind of things.

And unit propagation is one way of making sure that we get shorter clauses.

And short clauses are good because we are looking for the shortest of all possible clauses.

Okay. And we have two ways of making clauses short.

One is in essentially the deterministic way by doing resolution with a unit

that makes the long clause one shorter.

And we do that exhaustively and we kind of do that by making an assignment.

Think about CSP where we also made assignments.

Western Australia becomes red.

Whereas here we have variables for propositional true false like things.

So we make assignments like R is true and then we get kind of and we get literals in there

that will allow us to drop literals or to drop whole clauses,

which is wonderful because it makes actually things smaller.

That doesn't always work.

So we need a second rule, a splitting rule, which just basically is a case split.

We pick a variable.

We make it in one case.

We say, well, what happens if this becomes true and what happens if that becomes true?

And since we're simplifying with this, we get new units typically or hopefully.

We're going to choose P so that we're getting new units so we can propagate again

until we get stuck, then we split again and da da da da da da.

And by and large, this is extremely, extremely, extremely efficient,

especially because we have this unit propagation,

which really allows us to condense things down.

That's the procedure.

Very simple.

Pretty easy to implement.

And you'll end up with splitting.

You'll end up in these kind of binary trees.

They're kind of search trees for empty clauses.

They also may remind you a little bit about tableaus or so.

Turns out that these here are very efficient,

except that you can actually trick or annoy DPLL.

One way of doing that is having clauses like this.

A purely true clause with lots of variables and a purely false clause with lots of variables.

Those are 100 long, which means if we take care to fiddle things correctly,

then we'll have to do a splitting on every variable.

We look at this long clause, we split on every variable, that gives us a tree,

which we have to search fully, which has 2 to 100 nodes down here.

And if that's not annoying enough, we'll just, instead of 100, we use 1,000.

It's easy to make almost arbitrarily hard problems.

Fortunately, there are ways around that.

And that's what we actually didn't go into.