Discrete Mathematics for Computer Science

328 CHAPTER 5 Analysis of Algorithms

INPUT: a set C of clauses

OUTPUT: "satisfiable" or "unsatisfiable"

1. N for pal = F, T


2. set C1 = C


3. if pval = T


4. remove from C 1 all clauses containing Pi.

5. remove -'pl from all clauses in C 1 it occurs in

6. else


7. remove from C1 all clauses containing -Pl
   8. remove pl from all clauses in C 1 it occurs in


8. if C 1 is empty,
   output "satisfiable" and stop


9. else


10. for pal = F, T


11. set C 2 = C 1


12. if p al = T


13. remove from C 2 all clauses containing P2


14. remove -'p2 from all clauses in C 2 it occurs in


15. else


16. remove from C 2 all clauses containing -P2


17. remove P2 from all clauses in C 2 it occurs in


18. if C 2 is empty, output "satisfiable"


19. else

21.

22. for pvat = F, T


23. set • C, val= G-1


24. ifPn =T


25. remove from Cn all clauses containing Pn


26. remove -'Pn from all clauses in CG it occurs in


27. else


28. remove from CG all clauses containing -p,n


29. remove pn from all clauses in CG it occurs in


30. if CG is empty, output "satisfiable" and stop
    31. output "unsatisfiable"

(a) Trace through the execution of the code on the set C = {P3, -"P3 V P2, -P2 V

Pl} (so, for n = 3). Show what each Ci is after lines 8, 18, and 28. If the algorithm

stops with a "stop" command, say which step caused it to stop.