(20 pts.) 2SAT. 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 or the negation of a Boolean variable). You are looking for a way to assign a value true or false to 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 with five clauses and four variables: (x V) ^ ( V3) ^ (X1 V x) ^ (3 V X4) ^ (1 V x4). This instance has a satisfying assignment: set x, x2, x3, and x4 to true, false, false, and true, respectively. Given an instance of 2SAT with n variables and m clauses, construct a directed graph G = (V,E) as follows: Go has 2n nodes, one for each variable and one for its negation. Go has 2m edges: for each clause (a v) of (where a and 3 are literals), Go has an edge from the negation of a to , and one from the negation of to a. (a) Show that if Go has a strongly connected component containing both x and its negation for some variable x, then o has no satisfying assignment. (b) Now show the converse of (a): namely, that if none of Go's strongly connected components contain both a literal and its negation, then the instance & must be satisfiable. To prove this, show that the following algorithm results in a satisfying assignment: repeatedly pick a sink strongly connected com- ponent of Go. Assign the value true to all literals in the sink and assign false to their negations, delete all of the nodes in the sink, and repeat. (Hint: Consider case analysis on when each literal of a clause is assigned a value.) (c) Starting from a given instance of 2SAT, use everything discussed above to show that it can be solved in linear time.