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.