Use 2SAT to show that an implication graphs must have a cycle if it's not satisfiable

Question

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.

Answer 1

Here is a proof sketch. We will show that the given formula is unsatisfiable iff there exists a cycle containing both $x$ and $\lnot x$, for some variable $x$.

Suppose first that there exists a cycle containing both $x$ and $\lnot x$. The existence of a path $x \to^* y$ in the implication graph means that in a satisfying assignment, if $x$ holds then so does $y$ (you can prove it by induction on the length of the path). Since there is a cycle containing both $x$ and $\lnot x$, there are paths $x \to^* \lnot x$ and $\lnot x \to^* x$. In any satisfying assignment, either $x$ or $\lnot x$ holds, and both cases lead to contradiction.

Suppose next that there are no cycles containing both $x$ and $\lnot x$. We will construct a satisfying assignment as follows. Choose some variable $x$. If there is a path $x \to^* \lnot x$, assign $x = F$, and for each literal $\ell$ such that $\lnot x \to^* \ell$, assign the value to the underlying variable which makes $\ell$ true. You cannot be assigning the same variable two different truth values, since if $\lnot x \to^* y$ and $\lnot x \to^* \lnot y$ then also $y \to^* x$ and so also $\lnot x \to^* x$, completing a cycle involving $x$ and $\lnot x$.

If there is a path $\lnot x \to^* x$, assign $x = T$, and continue analogously.

If neither of these paths exist, assign $x$ arbitrarily, and continue as before. This cannot lead to a contradiction, for the following reason. Suppose that we assign $x = F$, and that there are paths $x \to^* y$ and $x \to^* \lnot y$. Then there is also a path $y \to^* \lnot x$ and so a path $x \to^* \lnot x$, contradicting the assumption that none of the two paths exists.

If after this process there is some unassigned variable left, choose one of them, and repeat until the assignment covers all variables.