This problem investigates resolution, a method for proving the unsatisfiability of cnf-formulas. Let ‑ = C₁ ∧ C₂ ∧· · ·∧C_m be a formula in cnf, where the C_i are its clauses. Let C = {C_i| C_i is a clause of ϕ}. In a resolution step, we take two clauses C_a and C_b in C, which both have some variable x occurring positively in one of the clauses and negatively in the other. Thus, C_a = (x ∨ y₁ ∨ y₂ ∨ · · · ∨ y_k) and C_b = (x ∨ z₁ ∨ z₂ ∨ · · · ∨ z_l), where the yi and zi are literals. We form the new clause (y₁ ∨ y₂ ∨ · · · ∨ y_k ∨ z₁ ∨ z₂ ∨ · · · ∨ z_l) 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 ϕ unsatisfiable. Say that resolution is sound if it never declares satisfiable formulas to be unsatisfiable. 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.