CODEWITHSUNDEEP
algorithmauthenticationsatsatisfiabilitydpll
nirvair
nirvair

Reputation: 4180

DPLL algorithm procedure

I am trying to understand DPLL procedure before actually coding it.

For example, I have these clauses: 

C1 : {c, !d, !b}    
C2 : {d, a}
C3: {b, !d, !a}    
C4: {d, c, b, a}    
C5: {c, !d, !b}    
C6: {d, c, b}    
C7: {c}

Now I take the decision variable as d = 0, b = 0. The clause looks like this now. 

C1: {c, 1, 1}
C2: {a}
C3: {1, !a}
C4: {c, a}
C5: {c, 1, 1}
C6: {c}
C7: {c}

How do unit propagation and pure literal rule play a part here?

Also, in C3 : {1, !a} - when I take a = 1, then this becomes {1, 0}. What should be the final value for this clause? Should it be {1}?

And if any clause has value {!b}, that is a negation of a literal, after applying the decision variable, then how to proceed?

Upvotes: 1

Views: 719

Answers (1)

user555045
user555045

Reputation: 64913

That step wouldn't have happened that way, because there were unit clauses in the input which would have been resolved first.

{ c } (the clause) is a unit and its literal c is positive, therefore c (the variable) is forced to be 1, then we have

C2 : {d, a}
C3: {b, !d, !a}

as active clauses, because true clauses are ignored.

Now b is a pure literal (it wasn't always, but it became one since some clauses are not active anymore), but practical SAT solvers usually don't check for that except during pre-processing since it can't be checked efficiently.

And finally you would set d or a or both it doesn't matter.

Upvotes: 1

Related Questions