Efficient algorithms for bounded-width RES. In lecture, we saw an Efficient algorithm for searching for space-bounded treelike resolution refutations. This is not the only family of proofs for which proof search is Efficient . A width-"w" resolution proof is one in which every line of the proof is a clause of at most "w" literals. In this exercise, you will show that for a fixed "w", there is an Efficient algorithm for searching for width-w refutations. Crucially, we do not assume that these proofs are treelike. Problem:

(b) Show that such an algorithm solves 2SAT (i.e., decides whether or not an input 2CNF has a satisfying assignment) in polynomial time. You will want to use the fact that resolution is complete for refutation of CNF formulas, i.e., there is a resolution refutation of every unsatis able CNF.