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

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.

• What did you try? Where did you get stuck? We're happy to help you understand the concepts but just solving exercise-style tasks for you is unlikely to achieve that. You might find this page helpful in improving your question.
– D.W.
Commented Mar 21, 2020 at 16:04
• Part (a) follows almost directly from the definitions. I challenge you to work it out yourself. You won't learn much by letting other people do exercises for you. Commented Mar 21, 2020 at 16:13
• I was able to solve part a, bit while part B seems intuitive I can't seem to formally describe this intuition to start a proof. Commented Mar 21, 2020 at 18:29
• You should show your progress so far and where specifically you got stuck, and read through the link I shared and use that to improve the question.
– D.W.
Commented Mar 21, 2020 at 19:04
• Hope it's better now! Commented Mar 21, 2020 at 23:18

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.