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
9. if C 1 is empty,
output "satisfiable" and stop
10. else
11.
for pal = F, T
12.
set C 2 = C 1
13.
if p al = T
14.
remove from C 2 all clauses containing P2
15.
remove -'p2 from all clauses in C 2 it occurs in
16.
else
17.
remove from C 2 all clauses containing -P2
18.
remove P2 from all clauses in C 2 it occurs in
19.
if C 2 is empty, output "satisfiable"
20.
else
21.
22.
for pvat = F, T
23.
set C, = G-1
• val
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.