Before we proceed to an algorithm, let's state a few important properties of the implication graph. The first one says that the graph is skew-symmetric. Formally, it means that if there is an edge from a vertex labelled by a literal l1 to a vertex labelled by a literal l2, then there is also an edge from the negation of l2 to the negation of l1. This is just by definition of this graph. So if we introduced an edge from l1 to l2, then we, at the same time, we introduced an edge from denegation of l2 to denegation of l1 and this also generalizes to paths in graph. If there is a directed path from l1 to l2, then there is a direct path from the negation of l2 to the negation of l1. This follows directly from the previous property about edges. To see this, let's consider the path from l1 to l2. So it contains several edges, it starts with l1 and ends with l2. Now consider the last edge, denote the variable, the beginning of this edge, for example. So we know that there is an edge from v to l2, which means that there is also an edge from the addition of l2. There's an additional fee, then consider second to last edge, assume that it is from u to v. The fact that there is an edge from u to v means that there is an edge I'm sorry, there should be a negation of v. There is an edge from the negation of v to the negation of u and so on by continuing in the same manner, we will finally reach the negation of the one. So once again, if there is a pass from l1 to l2, then there is also a pass from the negation of l2 to the negation of l1. The second property in a sense says that the implication is transitive. Namely, if a implies b and b implies c then a also implies c. More formally, the lemma says the following. Assume that there is a path from l1 to l2 in our graph. Assume also that we have a truth assignment that satisfies all the edges of our implication graph. Then l1 in this assignment, the value of l1 must imply the value of l2. That is, it cannot be the case that the value of l1 is 1, and the value of l2 is 0. To prove it, assume for the sake of contradiction that in our graph and in our assignment. L1 is assigned 1, and L2 is assigned 0. We know that there is a path and all edges are satisfied. So all the edges of this path are also satisfied. So we have a path where all the edges are satisfied and its beginning is labeled with one, and its end is labeled with 0. This means that actually there is a transition on this path where we go from 1 to 0. So there is some edge where which subject is beginning, is labeled with 1 and its end is labeled with 0. But this means that this edge is not satisfied, it is falsified. Again, recall that 1 does not imply 0, which leads us to a contradiction. The transitivity properties that we've just proved implies the following additional property. If we have two literals that stay in the same strongly connected component of the implication graph then they must be assigned the same value in many satisfying assignment. Why is that? Well consider two literals, l1 and l2. Assume that they stay in the same strongly connected component. because this is a strongly connected component of the implication graph. Assume for the sake of contradictions that there is a satisfying assignment which assigns the value of 1 to 1 of them and the value 0 to the other of them. For example, assume that l1 is assigned the value 1 and l2 is assigned the value 0. The fact that they lie in the same strongly connected component means that there is a pause from l1 to l2, but this contradicts to the fact that one must imply l2. So l1 and l2 if they stay in the same strong connective component must be assigned the same way. This in turn implies that if in the implication graph there is a strongly connected components that contain some literal together with it's negation, then this formula is answered justifiable. Because we cannot assign the same value to a literal and its negation. So if a strongly connected component of the implication graph contains a literal together with it's negation, we stop immediately and return that the formula is unsatisfiable. It turns out that this is the only case, when the input formula is unsatisfiable and we will prove it in a minute. As we have just discussed, the input formula is satisfiable if and only if, it's implication graph, I'm sorry, does not contain a strongly connective component, which contains a literal together with its negation. We still need to prove this property but using this property, we already ready to write down an algorithm. So the algorithm proceeds as follows. Given a 2-CNF formula F it first constructs the implication graph G of this formula. We then find the strongly connected components of this graph. Then we check whether some of the strongly connected components contains a variable together with its negation. If there is such a strongly connected component, we return immediately that the formula is unsatisfiable. This is because we know already in unstaisfiable assignment, all the literals lying in the same strongly connected component must be assigned the same value. And we cannot assign the same value to x and to its negation In the remaining case, we know that the formula is satisfiable. So the remaining part of the algorithm just constructs the corresponding satisfying assignment. For this we first find a topological ordering of all strongly connected components. Recall that the so-called meta graph or condensation or graph of strongly connected components is always a directed acyclic graph. Which means that we can find some topological ordering of all these strongly connected components. Then we process the strongly connected components in reverse topological agreeing. So we first place them on a line such that each edge goes from 1 going from 1 strongly connecting components to some other goals from left to right. And then we proceed these strongly connected components from right to left. For each strongly connected component, we consider the literals of the vertices staying in this strongly connected component. If they are not assigned yet, we assign them the value 1 and we assign the value 0 to all the negations of these literals. This way, we assign all the variables and from there we just return the correspondence of this final assignment. We still need to prove that this algorithm is correct, but we already know that the running time of this algorithm is linear in the size of the input formula, why is that? Well because we can assume that m is the number of clauses of the formula, clauses and m is the number of variables. Then the first step clearly takes running time n + n, because well we first introduced 2m vertices and then for each, for each of m, for each of m clauses we introduce three edges. So what we get is a graph on 2m vertices and 2m edges. The second step is also linear, we know that the strongly connected components of a graph can be found by just two calls to the [INAUDIBLE] search in linear time. This is also a linear step. So we just go through all the variables until each variable we checked wether variable and its negation lie in the same strongly connected component. The topological ordering of a graph can also be found in linear time. Finally, here we just process all the strongly connected components and at this step we can see that also all vertices of the initial graph shows is the step also takes linear time. So overall the running time of this algorithm is linear. We now need to prove that the y algorithm is correct. For this we need to show that our way of assigning values to all the variables satisfies all the edges. Recall that an edge is not satisfied in the only possible case when its beginning is assigned the value 1 and its end is assigned the value 0. So we want to prove that our algorithm avoids such cases. Well intuitively, it happens to avoid such cases, when there's the following. We process all our edges going from right to left, namely in the reverse topological ordering. And we always assign 1s to the right most available vertex. So we process the vertices, namely the strongly connected components containing our vertices from right to left nad we always assign the last available vertex the value one. This way we guarantee that basically we have zero's on the left and one's on the right, well very kind of wavy. More formally, we prove that when a literal is set to 1, that all the literals that are reachable from it, will name it all the literals that are reachable from it stay on the right. They are all ready assigned the value 1, and similarly when a literal is assigned the value 0, all the literals that this literal is reachable from have already been assigned the value 0. Well to be more formal, let me draw a little bit. So we would like to show that our algorithm, when assigned the values to all the variables, our algorithm avoids the following thing. That this variable is assigned zero, this literal is assigned zero, this literal is assigned one, let me denote them by u and v. So consider the situation when v was assigned 0 by a point of time when it was assigned 0 by algorithm. This means that at that point not v was assigned 1. Then we were processing all the strongly connected components from right to left and we've assigned 1 to the literal not v at this point. And this forces us to assign the 0 to v, but now this symmetry of the graph implies. That the results are a match from v through not u in our graph. And the fact that we processed all the edges from left to right means that u, that not u was assigned 1 also. But this means that you cannot date value 1, it was assigned the value 0 in fact. This is a contradiction, so this completes the analysis of this algorithm. Once again, we've just proved that our way of assigning the values to all the variables of the input formula satisfies all the edges and hence satisfies the input formula.