Efficient algorithms for bounded-width RES. In lecture, we saw an Efficient algo

Question

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.

Explanation / Answer

b)Proof-

Suppose there are path(s) x to x' and x' to x for some variable x in G, but there also exists a satisfying assignment p(x1, x2.... xn) for .

Case#1: Let p(x1, x2.... xn) be such that x=TRUE.

Let the path x to x' be x-> .... -> -> -> .... -> x'.

With the help of construction, there is an edge between A to B in G iff there is a clause (A' V B) in . The edge from A to B represents that if A is TRUE, then B must be TRUE (for the clause to be TRUE). Now since x is true, all literals in path from x to (including ) must be TRUE.

Similarly, all literals in the path from to x' (including ) must be FALSE (because x'=FALSE). This results in an edge between and , with = TRUE and = FALSE. Then,the clause (' v ) becomes FALSE, contradicting our assumption that there exists a satisfying assignment p(x1, x2.... xn) for .

Related Questions

Navigate

• Browse (All)
• Browse E
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.