This question is in

"Michael_Sipser_Introduction_Computation_Thomson"

Book

*7.13 This problem investigates resolution, a method for proving the unsatisfiability of cnf-formulas. Let o = C1AC2A... ACm be a formula in cnf, where the Ci are its clauses. Let C = {CC; is a clause of o}. In a resolution step, we take two clauses Ca and Co in C, which both have some variable r occurring positively in one of the clauses and negatively in the other. Thus, Ca = (x V y Vy2 V ... Vyk) and Co = (TV 21 V 22 V ... V z), where the yi and z are literals. We form the new clause (y1 V 42 V ... VYK V 21 V 22 V ... V zi) and remove repeated literals. Add this new clause to C. Repeat the resolution steps until no additional clauses can be obtained. If the empty clause () is in C, then declare o unsatisfiable. Say that resolution is sound if it never declares satisfiable formulas to be unsatisfi- able. Say that resolution is complete if all unsatisfiable formulas are declared to be unsatisfiable. a. Show that resolution is sound and complete. b. Use part (a) to show that 2SAT P