In the backtracking algorithm for SAT, suppose that we always choose a subproblem (CNF formula) that has a clause that is as small as possible; and we expand it along a variable that appears in this small clause. Show that this is a polynomial-time algorithm in the special case in which the input formula has only clauses with two literals (that is, it is an instance of 2SAT).

A backtracking algorithm is aproblem-solving algorithm that uses a brute force approach for finding the desired output.The Brute force approach tries out all the possible solutions and chooses the desired/best solutions.

The term backtracking suggests that if the current solution is not suitable, then backtrack and try other solutions.

$X$Let us first consider an example, say the following formula $\phi$.

$(X\vee Y)\wedge (Z\vee \neg Y)\left(X\right)(\neg X\vee \neg Y)(W\vee Z)(\neg Z\vee W)(\neg U\vee \neg W)(\neg Z\vee U)$

To understand why the proposed algorithm solves 2-SAT in polynomial time, let us see what happens

Since$\phi$ is satisifiable if and only if is assigned true, we get a residual formula –

$(Z\vee \neg Y)(\neg Y)(W\vee Z)(\neg Z\vee W)(\neg U\vee \neg W)(\neg Z\vee U)$

Note that every clause that remains is either a unit clause, or was present in $\phi$originally. In general, this is also the case,

if all the clauses of the same size, we chose just one variable randomly and then expand on it, and get that every clause that remains is either a unit clause or was present in $\phi$originally.

When unit clauses are present, we expand on those variables, by the algorithm. In this example, we see that Y must be assigned false, and expanding we get: 2

$(W\vee Z)(\neg Z\vee W)(\neg U\vee \neg W)(\neg Z\vee U)$

Again, the remaining non-unit clauses were all present in$\phi$ ;

in fact, this must be the case since the algorithm modifies clauses by deleting literals. Crucially, because of this fact, the residual formula is satisfiable if and only if$\phi$ was. Thus, there is no need to backtrack, and 2-SAT can be solved by a linear sequence of linear expansions.

In the original backtracking algorithm, this corresponds to skipping the second call to expand whenever the first call returns a non-empty result.