Using 2SAT and implication graphs, how could I prove the following properties of implication graphs:
Suppose there is a directed path between literals l1 and l2 in G_φ. Then there is also a directed path between their complements. Then, there is τ, a truth assignment satisfying φ where τ(l1) is true, then τ(l2) must also be true.
Using this, show that φ is unsatisfiable <=> there is some directed cycle in G_φ containing a variable x and its complement.
Where G_φ is the directed implication graph of 2SAT containing formula φ with n variables. Hence 2n vertices with one for every possible literal in φ, and edges (not l1, l2) and (not l2, l1) for every clause (l1 ∨ l2) in φ.
My first intuition was a proof by contradiction however I failed to construct a general enough assumption. I then tried to show that if the truth assignment means that l1 and l2 are true, then by building a cycle connecting all variables, the assignment is only valid when those edges exist. However this doesn't seem rigorous enough since I'm not properly understanding why the cycle requires the complement of x to exist.
Currently I build G by adding a vertex for every variable x and it's complement as well. Then for each clause (a v b) I add an edge between not a and b and not b and a.
However I fail to see how this would specifically form a cycle.
Working of the sipser textbook.