Original subtitles

hello everybody so we're going to now move on to the dpll algorithm

so this is a complete algorithm for solving satisfiability for propositional formulas

based on two recipes the first one is search we use depth first search and the second recipe is

deduction we use a simplified version of resolution that we saw earlier this week

called unit resolution this algorithm was first developed by um davis putnam yeah so the so-called

dp algorithm so this uses only the deduction part of the algorithm but then later on davis hired the

program as logan and laughlin to implement this algorithm and found out that this was not this

was too memory intensive to yield a an efficient algorithm and therefore the programmers discovered

that combining it with search namely depth first search

was a good way to make this algorithm more efficient and more amenable to implementation

so uh this is basically the version that we're going to see this dpll algorithm so there's

a little history behind it so dpll is also the basis for modern set solvers today um which uses

the so-called cdcl algorithm and um which this enhances dpl with very many heuristics like close

learning non-chronological backtracking and this a lot of these heuristics we're gonna see if you're

interested we're gonna see um we're gonna cover we cover this thing in the course automated reasoning

so contact me if you're interested um also one one thing one more thing to say is that

we only gonna cover in this lecture a recursive a recursive version of dpll which is a simpler

version of dpl it has all the um all the basic ideas of the pll but it's uh more memory

intensive than the iterative version of that okay which we're not gonna cover in the course

okay so to start with let's talk a little bit about the a simple depth first search algorithm

for solving satisfiability here of course we don't need the formula to be in cnf so

basically what it does here is you have an enumeration of the variables

and then you go through this variables one by one and then assign it by zero

or one yeah by zero or one and then when you hit unsatisfiability you go you you backtrack

and then you flip the assignment and so on and so forth so you want to enumerate all the possible

all the possible assignments so what makes this different from uh the truth table uh yeah by just

by using a truth table the main difference here is simply the the boolean short circuit or here

and and what what what's going on here is that when you when let's say the left part is already

uh it's already satisfiable you will then just return true yeah without actually having to

go through the right part of of the boolean or here okay so this is a short circuit it

might save some time so this is of course um yeah i mean this is uh probably more efficient

can be more efficient in some cases than just enumerating all the possibilities yeah

also if you just try to take a look at the details here this is written in a python style pseudocode

so you can see here you have this is recursive in particular you check if the formula is top

or bottom so there are the two cases here and then after that if it's not top or bottom so

it means there's a variable you just use one of the variable and then you assign

zero or one to it okay and then you then recurse on the function okay so um let's take a look at uh

let's try to apply this algorithm on this example so let's say we start with x equals zero

yeah x equals zero and if you simplify this thing you'll realize that this actually ends up with

bottom you don't really know you don't really need to know what the y is in fact yeah you already can

say that this is in fact this is equivalent to um it's already equivalent to bottom all right so um

then we don't really need to continue it means so we just have to go we just have to go back now

and then say okay so that's not good now we're gonna check if it if x equals one all right so

in this case we have uh y so we simplify we assign 0 to x yeah and then we do the simplification

so we get y and not y okay of course if you just assign y equals 0 or 1 here in both cases you will

get bottom as well yeah so after you get here from here you go back to the initial uh the top level

of the recursion and you say it is unsatisfiable but i think the the thing that i wanna

uh the message here is that you do actually save some time

if you're actually just using truth table you will have to assign every single um i'll have to

go through every single assignment but in this case you don't actually need to go through the

case of y equals zero or y equals one is where you already know that it is unsatisfiable right so um

yeah so the so the main point here is that this is actually faster than truth table

in some cases yeah so um here i just wanted to say here if you have a term

that is what is a term so a term is a conjunction of a conjunction of um of literals yeah if you

if you use this if you use this uh if you use this algorithm then this will run in actually will run

in polynomial time on on terms yeah conjunctions of literals but truth tables you will you have to

uh this will have to run in exponential time i mean this is all i meant here in the note

okay so um that's the search part of dpll so let's take a look at the second part which is the uh

the deduction part of the dpl and as i mentioned this is a simplified version of resolution

the so-called unit resolution and this rule can be summarized as follows

using this using this uh this tableau here basically what it says is that we apply we

try to produce a resolvent yeah by taking one of the one of the one of the clauses in the

one of the two clauses that we need to take to produce a resolvement must be a unit clause a unit

clause means a clause consisting only of a single literal so in this case is this bit here yeah okay

um so here's a little example so suppose you have two clauses so the clause

x here and the clause not x y not z and if you apply this rule this unit resolution basically

you apply it just like you apply resolution so you take you remove the you remove the um two opposite

literals which is x and not x here yeah and then you just take this the remaining literal which

is y and not that okay so that's basically unit resolution it's simpler than a normal resolution

so here's a little example of unit resolution um so as you can see here there's only one way

to apply unit resolution at the beginning you just have to pick a unit literal which is this

only one option which is this one right p um so in this case there's actually also only one

option you have to pick this one because this is only p and not p area so in this case you

produce q now you can then apply another unit um another unit resolution by applying this this

um and that yeah and then you get r commas yeah so that's basically the end of uh

um so you can apply unit resolution several times and this procedure

where you apply unit resolutions repeatedly this is called boolean constraint propagation bcp so um

and that's basically the underlying one of the underlying procedure uh sub procedure behind

the depela algorithm so so here this dpl algorithm is simply a modification of the dfs

algorithm for satya the one that we saw earlier by having this line here before you

go through this you try to assign true and false etc you just try to simplify the formula first by

applying unit resolution as much as possible yeah so let's take a look at some examples

so here is a little formula with four um oh actually one one thing i need to

note here quickly in this case uh you do need the formula to be in cnf otherwise this will not

work yeah this bcp thing i mean this is unlike of course unlike the dfs algorithm which would work

regardless whether or not the formula the input formula is in cnf

okay so let's take a look at this example here a formula with four clauses

um right so

if you apply if you try to apply dpl the first thing that we notice is that we cannot actually

in the beginning we cannot apply bcp right because there is no unit clause so for this reason we will

have to branch yeah so this branching here it means that we will have to consider q equals

let's say well i mean you have the sine of uh one or zero to one of the variables basically right

and here the choose variable function let's say it returns q okay so we just pick a variable

let's say q and let's say q equals one and we consider two cases we split two cases q equals

one and q equals zero let's take a look at the left case first in this case we assign one to

zero so this is the simplification so the if you assign one of course this because this is a

this is a clause so each clause here for example this one if you assign one

it means that the entire clause is true so you remove it you don't actually need to consider

that because it's or yeah remember so this is gone and then you only consider the cases where

the uh the clause the clause the remaining clauses that are not um there are that were

not made true by this assignment okay so in in which case we have this uh the second one here

so you assign zero here so you only have r and then also you have not r and you have p and not

r yeah okay so that's uh the resulting um the resulting formula after assigning q to one

now what do we have next well we see now that we can actually apply unit resolution here yeah

so uh in fact if you just apply if you just uh take this r and not r you will immediately

get a contradiction you will immediately derive the empty you will immediately derive the empty

the empty clause okay so you use bcp here by resolving this so you get empty clause

and of course if you get an empty clause you remember that we um basically this is already

unsatisfiable and if you just let's say go back again to the procedure here so if this gives

you unsatisfiable basically you get here and you're gonna return false yeah so you're gonna

basically that's what you get here if you return false but then if you return false then you have

to it means that you have to consider the other cases because you split you've only considered one

case that is q equals one now we can consider the second case that is q equals zero yeah

so if in this case when you assign q equals zero we do the same thing and the remaining

in fact clause here are not clauses only have one plus left because the other clauses have

been made true by this assignment so you have not b comma r yeah now what do we have here

so in this case not p comma r we don't actually have a unit clause so we have to do assignment

again we have to assign uh something to p and also to r so let's just say that we make the assignment

now p equals zero p equals one if p equals zero um this is actually already true yeah so actually

you could you could have stopped here and you don't need you don't actually need to to continue

because you already know that there's something that already makes this entire formula true

yeah but let's just say for our for an argument's sake we just look at the other cases yeah so we

get uh if you look consider the case of r equals um so if you let's say start with p equals one you

get this yeah and then you have to assign r equals zero or r equals one and then you get uh in this

case you get false in this case you get uh you got a bottom and you got top yeah so in any of these

cases where you get top you would the procedure will return um satisfiable and will return true

to um we'll say that the formula is satisfiable okay so that's the um that's the example

and of course you can read a solution so so if you have a path from um if you hit

a top at the end you can actually then read off the solution from the path from the root

to the leaf yeah by just reading the um by just uh by just taking a look at the um

uh so we just have to look at the assignments that you make for um for the for the variables

um here's a little simple improvement that you can make this is uh basically already this was

already proposed by davis and putnam initially before loggerman and laughlin came around and

introduced the improvement using dfs yeah so this is the so-called pure literal rules

so what is what is going on here so appear so um we say that a literal

yeah a literal basically x or not axia we say that a literal is pure if it appears only positively or

negatively in the formula okay so it means only positively or only negatively in the formula

so what is so special about pure literals we can simply yeah we can make them true before

we choose a decision variable to branch yeah so so because we we know that it only appears either

only positively or only negatively so basically you say like okay so let's say if it only appears

positively we just make this uh we just make x true yeah if it only appears negatively we just

makes x false and this will save some time um so you so that you don't have to consider the case

of x equals true or x equals false and you will we'll see in a we'll try to apply this to the

example that we just saw just now um okay before that let's just uh summarize the algorithm here

with this pure literals so basically what's going on here is that

you apply pure literals these pure literal rule which is uh written

here yeah set pure true we just set all the pure literals to be true

and we also apply the bcp algorithms um repeatedly okay in turn and and we break when these two

when these two procedures set pure true and bcp do not change the formula at all okay

so this is basically the only addition to it so you just add this set pure true so

so this is the example that we saw just now so this is the entire tree

so let's see what the tree looks like when we apply this sub-pure true in this in this case

the tree looks like this if we apply the set pure true so when so we so

we go through this from start to finish so from start so remember initially we try to see like

here yeah we try to see that uh the formula you can apply bcp to the formula and you say no

you can't apply bcp but can you apply pure um the set pure true here and then you check like okay

um what about p so p appears both positively and negatively so here positive and negative so that's

not a pure literal p is not a pure literal yeah pure not p is not a pure literal uh what about q

q here negative positively and negatively so that's not pure what about r the same yeah

so you can see r and not r here so you can also so you also you cannot apply this set pure true

so this means that you still have to do the branching without actually this this

it means it doesn't make a difference at the top level so you

um so this is fine so i'm not going to cover this bit so let's just cover this bit here yeah so

this is the the part or the second part that's kind of where it's going to make a difference

so in this case so if you take a look at this what's going on is that well so for this

clause here or for this formula here you see that both not p and r are actually pure literals at the

step yeah um in this step so you can simply make this pure literal true so for example

um not p is your pure literal so you just make p true that is we set p to be zero um so we just

apply this thing and then we get a top okay so we don't have to you can you can see the two cases

here so this can be for example can be big like this but in this case you only get a single um

so you actually save some time like having to go through some of the some of the combination of

b and r yeah so it can be pretty handy sometime to apply this and that's just one example right

so that's pretty much it i have to i have some exercises for you um to exercise in fact and uh

yeah try to spend some time to go through this try to apply both the pll with or without the

pure literal rule and see how you can um how this uh how you can solve this thing yeah so

also try to look at different combination of um the choose variable strategy yeah in which

order it can be better and for which example when you well actually in the final exam can be handy

when you try to do this yeah because if you know how to do this well then it can be faster for you

okay so we'll go through the solution at some point okay so we're gonna now talk about how to

implement dpll efficiently in particular we're going to talk about boolean constraint

propagation how to implement this efficiently because like it or not the main bottleneck of

this algorithm the depel algorithm is really in the frequent use of bcp and unit resolution so

one rule that is really important is the so-called deleting redundant clauses rules and this consists

of two different rules sub proofs the first one is that we want to delete all clauses containing

the unit clause that is suppose we want to apply unit resolution on the unit clause

on this unit clause here so we want to do what we want to do is that after we finish applying

all unit resolutions involving this unit clause we want to delete this unit clause

all right and the second one is that we want to delete all occurrences of the negation of l from

the other classes so let me just first show you um before i explain to you why this is the case

why this is okay to do let me first explain by an example say we have the full example here

and we in this case we have to apply um unit resolution involving this clause here

so what you do here in this case you only have a chance to do it with this one for

example yeah so this and that so in this case you need to then delete these clauses here

and then after that what you do next is you're gonna then delete the not l from the other

clauses which is in this case this is their the only remaining one so the question is why can we

um why can we do this why can we delete these clauses so one thing is

in order to understand this it is important to perhaps reformulate a little bit what we are

really doing when we do this unit resolution and boolean constraint propagation so every time we do

boolean uh every time we do unit resolution yeah let's say involving this unit clause

oops involving this unit clause l here what we're really doing is that because this is

a clause and this contains only of a single literal and we have a formula in cnf

what we have to do here is in order to keep this in order to keep this formula satisfiable

the satisfying assignment must set l to be true you have no other choice right this is what you

have to do and if you set l to be true of course all the other of course all the other l and the

all occurrences of l everywhere else is going to be true and for example in this case here

if you set this thing to be true this is gone why is this gone because this is a clause a

clause is a disjunction of stuff as soon as one of the literals is true it's true right so it's

gone in the sense that you know it's no longer is it's no longer a problem so it's true so we just

we just get rid of it yeah so we are only worried about it when this is false not when it's true

because you have the conjunction of clauses yeah so if you have one of the conjuncts is

true you just simply get rid of it you don't care about it so this is basically what's going on

you set l to be true so all the clauses containing l you just simply remove them all right and by the

same token you have the not l as well for example this one here yeah so if you set out to be true of

course not all has to be said to be false yeah so in this case uh again remember a clause you have a

um it's a disjunction of literals so as soon as if you have one of if one of the literals is false

and you have a disjunction it doesn't matter right so you just have to simply remove

this literal yeah all right so this is basically what you're doing here as well

okay so that's basically the reason why we can remove the clauses uh while we can do this

to why we can do these two rules here because they preserve satisfiability yeah and this is

for um this is formally stated in this proposition so if you have a formula of this form that is

one of the so your formula in cnf and one of the clauses is a unit clause let's say l containing

of only of l here then of course you have to set l to be true so in that case you simply just set

l to be uh replace l by true but by top sorry and then you replace not l by bottom yeah so this is

has this has to be equally satisfiable yeah so um yeah so this i've explained to you why this

is the case and i encourage you to try to write down the formal proof of this um the main idea

as i've already just described yeah so um now the next thing of course is uh okay so we can do this

this sounds good but how does this affect the complexity of boolean constraint propagation why

does this make things faster the main reason why this makes things faster is that with the deletion

rules that we just mentioned the number of clauses kept in the memory will never really grow yeah so

each application of unit resolution will remove will remove one of the one of the clauses yeah

and the unit clause yeah and for the other clauses the what's really going to happen is

that you're just simply going to remove one of the literals from them okay so you don't really

add new colossals to this to this formula okay so this is why you can essentially the reason

why you can implement this thing in polynomial time and also if you want to make this faster

you can actually make this you can actually implement this in linear time in fact

and this you can be done by help of hash maps so you can for example take a couple of hash maps as

as described here you can have a hash map from formulas to um so from formulas to

the corresponding clauses so basically let's say you index the clauses one two

three et cetera in this case you you have one two let me just write down here so one two three

etc here and you also have a map from from the literal to the claw so for example here you map it

here and this you map it here etc so this is this will help you so as soon as you for example need

to delete not p you just simply have to look at this uh lookup table the hashmap and then you then

get mapped to the corresponding the corresponding clauses to delete them etc yeah so this is um this

basically then you don't really need to go through the entire set of clauses so you can simply go

directly to the the clause that you really need to modify and finally you have a set of keys for

f for unit classes that is this one yeah so this is basically um this will help you to

trigger the corresponding unit clauses that you have to apply

all right so um yeah so i um this is one of the main one of the possibilities um if you want to

implement this thing in linear time there are of course other ways to do it but the important

thing is yeah you need to use some kind of hash maps and maybe you can decide several of them

okay so um i'll just say something i'll just say really quickly about correctness of dpll

so in order to prove correctness of dpl you need to prove termination and partial correctness

namely that the algorithm terminates and partially correct correctness means if it terminates it will

output the right thing um so the proof of this is actually not really difficult but

if you want to write down in detail it actually can be a little bit long but in order to prove

correctness what you really need to do is just to observe that all the subroutine yeah that is bcp

sub pure true and dfs here all of this um all of this terminate yeah so one thing that is important

of course with vcp is uh yeah i mean this is a again as you saw it's a kind of uh um this

is a kind of a fixed point it's kind of a fixed point thing and this is um when you implement

this together with sad pure true is also kind of a fixed point thing as well so you can sort of use

an argument related to you know that that you will reach a fixed point yeah so for dfs i mean this is

uh i guess um there's nothing much to say about this thing because you really just enumerate all

the all the possibilities and finally for partial correctness yeah i mean this you can try to argue

by induction on the size of the formulas yeah and so on and so forth so um yeah i think i want to

stop here and again i want to mention that i want to emphasize that we've only looked at the

recursive version of dpl of dpll yeah and this is not the most efficient version of dpl

the reason of course the reason behind it is that if you use recursion there's an implicit implicit

stack and every time you need to go to the next level of the recursion you need to copy things

you need to copy the entire formula which can be quite large and this is quite expensive so

if you want to make this fast you need to turn this into an iterative version of the algorithm

and in order to do that i encourage you to take a look at some of these

references and of course these references also contain

the the algorithm the cdcl algorithm that i that we mentioned at the beginning of the lecture

yeah and um i especially encourage you to look at this one if you're interested