0:00

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.

Â 1:24

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.

Â 2:27

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.

Â 4:53

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.

Â 7:55

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,

Â 9:44

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.

Â 11:53

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.

Â