# the correctness of 2-satisfiability problem algorithm by using implication graph

I learned finding a solution of 2-sat problem algorithm below.

The point are below

(1) when constructing the implication graph

(2) finding there is no occurrence of a variable x and its negation x' in any SCC in the graph.

(3) then there is always the solution at this 2-SAT problem.

it means that all false 2-SAT problem have a variable x and its negation x' in SCC of its implication graph.

I cannot understand this point (3).

How can I prove it has a solution if only if there is no x and x' in a SCC?

It looks like to me, although there is no x and x' in SCC, it can be false. • Asked at least once on this site. Probably covered in many lecture notes. May 14 '20 at 12:32
• @YuvalFilmus Thank you for your comment! Then, I'll try to find the answer, and then delete this post or add the answer to this post. May 14 '20 at 12:35
• cs.stackexchange.com/questions/117764/… May 14 '20 at 16:49
• @KyleJones I really thank you so much. your answer means "At unsatisfied 2-SAT instance, we can see X value change 0, 1, 0, ... again according to our effort to satisfy this instance. it means circular implication (x and x' in the SCC simultaneously)." Is it right? Do I understand it properly? May 17 '20 at 9:29
• Yes, that is correct. May 17 '20 at 13:17