My task is to solve the 2SAT problem.
I have read online that a good method to solve this problem would be to construct an implication graph, where each statement of the form
A || B implies two edges
~A -> B and
~B -> A. Then, we can set values to each variable by finding all the strongly connected components of the graph.
However, this input is confusing to me:
1 || 2 ~1 || 3 4 || ~2 (each line represents one or statement: ~ means "not")
When I draw the implication graph for the above input, the graph looks like this:
~3 -> ~1 -> 2 -> 4 ~4 -> ~2 -> 1 -> 3
The reason this confuses me is because there are no strongly connected components in this graph at all, meaning that the strongly connected component algorithm wouldn’t find any components, which means that we wouldn’t be able to set values for the variables. I don’t know if I’m misunderstanding the algorithm itself, or if I’ve drawn the graph wrong. Can somebody please help me understand my mistake?