1

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?

Guy Coder
  • 24,501
  • 8
  • 71
  • 136
nirvair
  • 4,001
  • 10
  • 51
  • 85

1 Answers1

1

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.

harold
  • 61,398
  • 6
  • 86
  • 164
  • So, what should be my first step when I see a unit clause? – nirvair May 06 '17 at 20:53
  • And if `c` becomes 1, then C7 would be {} or {1} ? – nirvair May 06 '17 at 20:56
  • @nirvair C7 would be {1} but since it contains a {1} it will become inactive. When you have a unit, do unit propagation. – harold May 06 '17 at 21:28
  • I have not actually understood how unit propagation works. – nirvair May 06 '17 at 21:50
  • Conceptually, replace positive uses by 1 and negative uses by 0, then simplify (remove 0's from clauses, remove clauses that contains 1). Practically it won't work like that, because doing it naively would take far too much messing about with data structures, it would be slow. You should probably check the literature if you're serious about writing a SAT solver, it's a big subject. – harold May 06 '17 at 21:55
  • So, the final result that I get is: c = 1, b = 0, a = 0, d = 0. And the only literal with unit propagation is `c`. And with the pure literal rule, we get `b` as pure literal. Is that correct? – nirvair May 06 '17 at 22:15
  • @nirvair those should all be 1, if done that way. Pure literals should of course be made *true*, not false. – harold May 06 '17 at 23:00
  • In that case, what are other literals along with b that satisfy the clause with Pure Literal Rule? First, c=1, then d=0, then a is unit literal which makes a=1, then all the clause sets are 1 when b=0 or b=1. Is this step correct if I am trying to solve the problem manually? – nirvair May 07 '17 at 18:21
  • Let us [continue this discussion in chat](http://chat.stackoverflow.com/rooms/143623/discussion-between-harold-and-nirvair). – harold May 07 '17 at 18:22