Solution Found!
In the backtracking algorithm for SAT, suppose that we always choose a subproblem
Chapter 9, Problem 9.1(choose chapter or problem)
In the backtracking algorithm for SAT, suppose that we always choose a subproblem (CNFformula) that has a clause that is as small as possible; and we expand it along a variable thatappears in this small clause. Show that this is a polynomial-time algorithm in the special casein which the input formula has only clauses with two literals (that is, it is an instance of 2SAT)
Questions & Answers
QUESTION:
In the backtracking algorithm for SAT, suppose that we always choose a subproblem (CNFformula) that has a clause that is as small as possible; and we expand it along a variable thatappears in this small clause. Show that this is a polynomial-time algorithm in the special casein which the input formula has only clauses with two literals (that is, it is an instance of 2SAT)
ANSWER:Step 1 of 3
Let us first consider an example, say the following formula \(\phi\)
\((X \vee Y) \wedge(Z \vee \neg Y)(X)(\neg X \vee \neg Y)(W \vee Z)(\neg Z \vee W)(-U \vee \neg W)(-Z \vee U)\)