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.

enter image description here

  • $\begingroup$ Asked at least once on this site. Probably covered in many lecture notes. $\endgroup$ – Yuval Filmus May 14 '20 at 12:32
  • $\begingroup$ @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. $\endgroup$ – nimdrak May 14 '20 at 12:35
  • $\begingroup$ cs.stackexchange.com/questions/117764/… $\endgroup$ – Kyle Jones May 14 '20 at 16:49
  • $\begingroup$ @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? $\endgroup$ – nimdrak May 17 '20 at 9:29
  • $\begingroup$ Yes, that is correct. $\endgroup$ – Kyle Jones May 17 '20 at 13:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.