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.