threshold for random 2-sat

Question

I'm looking at notes on the threshold for random 2-sat which is given as $r_{2}^{*}=1$.

In the first part of proving the threshold they claim that a 2-sat formula is satisfiable if and only if the graph of implications does not contain a cycle containing a variable and it's negation. In the calculation it says the following

"We will actually work with a slightly stronger sufficient condition, namely: the formula is satisfiable if it does not contain a bicycle, which is defined as follows."

Definition 7.6: For $k ≥ 2$, a bicycle is a path $(u,w_{1},w_{2},...,w_{k},v)$ in the graph of implications, where the $w_{i}$’s are literals on distinct variables and $u, v ∈ \{w_{i}, \overline{w}_{i} : 1 ≤ i ≤ k\}$.

I can understand the calculations they use given this fact, but can someone try and give an outline of why it's true that if the graph of implications of a 2-sat formula does not contain a cycle then the formula is satisfiable? Or equivalently if a forumula is not satisfiable then it contains a bicycle.

Answer 1

The implication graph tells you that 'if $x$ is false, then $y$ has to be true' to make some litteral true, and therefore the formula true. So if you have a bicycle, it means that you have a sequence of implications that say that for some $w_i$, $w_i$ has to be true and false to satisfy the formula. Since this is a contradiction the formula is unsatisfiable.

Answer 2

Let $C$ be a $2$-CNF formula. We prove that if $C$ is unsatisfiable then there is some variable $x$ such that $x$ is reachable from $\bar x$ and vice versa in the implication graph $G(C)$. The proof uses induction on the number $n$ of variables in $C$.

Base case. If $n = 1$ then $C$ must contain clauses $x \vee x$ and $\bar x \vee \bar x$ and hence the edges $(x, \bar x), (\bar x, x)$ are in $G(C)$.

Inductive step. Let $C$ has $n > 1$ variables. Choose some variable $t$ such that either $t$ is not reachable from $\bar t$ or vice versa (if there is no such variable then the statement holds). Assume the latter case and let $Q$ be the set of vertices reachable from $t$, we have $\bar t \notin Q$. If $q \in Q$ then $\bar q \notin Q$. For otherwise there are paths $P_1$ and $P_2$ from $t$ to $q$ and $\bar q$ respectively. By reversing $P_2$ (using contraposition) we obtain a path from $q$ to $\bar t$ and hence we have a path from $t$ to $q$ to $\bar t$, that is $\bar t \in Q$, a contradiction.

Let $V(Q)$ be the set of variables with $x \in Q$ or $\bar x \in Q$. Let $V(Q) = \{x_1, \dots, x_{|Q|}\}$. Define a mapping $v \colon V(Q) \to \{0, 1\}$ to be the (partial) assingment with $v(x_i) = 1$ if $x_i \in Q$ and $v(x_i) = 0$ if $\bar x_i \in Q$. This assignment $v$ satisfies all clauses $K$ having at least one variable in $V(Q)$. For assume $p \in V(Q)$. Let $K = p \vee q$, then $K$ is satisfied by $v$ since $v(p) = 1$. If $K = \bar p \vee q$, then we have $q \in Q$ since $K$ produces the edge $(p, q)$ in $G(C)$ and $p$ is reachable from $t$. So $v$ satisfies $K$ since $v(q) = 1$.

Finally, denote by $C'$ the new $2$-CNF formula obtained from $C$ by the removal of all clauses containing a variable in $V(Q)$. Note the following:

1. $G(C')$ is a subgraph of $G(C)$.
2. $C'$ is unsatisfiable since $C$ is, while all removed clauses are satisfiable by $v$.
3. $C'$ has $n - |Q|$ variables (and $|Q| > 0$).

Hence by the inductive hypothesis there is a variable $x$ in $C'$ such that $x$ is reachable from $\bar x$ and vice versa in $G(C')$ and hence (by 1.) the same holds for $G(C)$.