How Tarjan algorithm work for the 2-SAT

Question

Tarjan's algorithm for 2-SAT is based on the truth:

a 2-CNF formula is satisfiable if and only if there is no variable that belongs to the same strongly connected component as its negation.

But I don't find any reason for the right to left direction. how can the inexistence of such variable guarantee satisfaction of CNF?

I tried to follow the steps of the algorithm, and I was stuck here:

For each component in the reverse topological order, if its variables do not already have truth assignments, set all the literals in the component to be true. This also causes all of the literals in the complementary component to be set to false.

Isn't it possible the variable is already assigned WRONGLY? When we keep assigning TRUE from the back, and we assign the FALSE in the middle, but the TRUE is to be assigned to the next variable. In this case, the feasibility breaks.

Of course this kind of case never happens because the algorithm is right and many people use this algorithm well. But so many post says it as the trivial things.

• I think the reason why those assignment is possible is relevant to the skew-symmetric condition of the graph, since (x -> ~x -> y -> ~y) never has true assignments.

Answer 1

a 2-CNF formula is satisfiable if and only if there is no variable that belongs to the same strongly connected component as its negation.

But I don't find any reason for the right to left direction. how can the inexistence of such variable guarantee satisfaction of CNF?

Think of a variable assignment for some unsatisfiable 2-SAT instance. This means one or more clauses must remain unsatisfied whatever the assignment. You change the setting of one or more variables to satisfy those clauses, but this unavoidably leaves some new clause or clauses unsatisfied because the instance is unsatisfiable. The failure of your change to satisfy the instance implies that some other variable's value must change. You repeat the procedure again and again, changing other variables as implication demands, but never succeed in satisfying all the clauses. Eventually, because the number of variables is finite, a failure implies that you change the value of a variable you've already visited... and that is your circular implication from $x$ to $\bar{x}$ back to $x$. Without a circular implication you will eventually reach the end of the implication chain and have a satisfying assignment. The only way not to reach the end of the chain is for the chain to be circular between a variable and its negation.