In the 2SAT problem, you are given a set of clauses, where each clause is the disjunction (OR) of two literals (a literal is a Boolean variable of or the negation of a Boolean variable). You are looking for a way to assign a valuetrueorfalseto each of the variables so that all clauses are satisfied- that is, there is at least one true literal in each clause. For example, here’s an instance of 2SAT:
This instance has a satisfying assignment: set and totrue, false, false,andtrue,respectively.
- Are there other satisfying truth assignments of this 2SAT formula? If so, find them all.
- Give an instance of 2SAT with four variables, and with no satisfying assignment.
The purpose of this problem is to lead you to a way of solving 2SAT efficiently by reducing it to the problem of finding the strongly connected components of a directed graph. Given an instance l of with n variables and m clauses, construct a directed graph as follows.
- has nodes, one for each variable and its negation.
- has edges: for each clause of l (where are literals), has an edge from the negation of to , and one from the negation of to .
Note that the clause is equivalent to either of the implications or . In this sense, data-custom-editor="chemistry" records all implications in l .
(C). Carry out this construction for the instance of given above, and for the instance you constructed in (b).
(d). Show that if has a strongly connected component containing both and for some variable x , then l has no satisfying assignment.
(e). Now show the converse of (d): namely, that if none of ’s strongly connected components contain both a literal and its negation, then the instance l must be satisfiable.(Hint: Assign values to the variables as follows: repeatedly pick a sink strongly connected component of . Assign valuetrueto all literals in the sink, assignfalseto their negations, and delete all of these. Show that this ends up discovering a satisfying assignment.)
(f). Conclude that there is a linear-time algorithm for solving 2SAT.
