All language subtitles for dpll

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