Use 2SAT to show that an implication graphs must have a cycle if it's not satisfiable
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.