TAOCP 7.2.2.2 Exercise 200
Let the implication digraph of a 2SAT formula have one vertex for each literal.
Section 7.2.2.2: Satisfiability
Exercise 200. ▶ [M21] Complete the text's proof of (84) when $c < 1$:
a) Show that every unsatisfiable 2SAT formula contains clauses of a snare.
b) Conversely, are the clauses of a snare always unsatisfiable?
c) Verify the inequality (89). [Hint: See exercise 199.]
Verified: no
Solve time: 2m24s
Solution
Let the implication digraph of a 2SAT formula have one vertex for each literal. A clause $(a\vee b)$ gives the two implications $\bar a\to b$ and $\bar b\to a$. An $s$-chain $C=(l_1,\ldots,l_s)$ gives the clauses
$$ (\bar l_1\vee l_2),(\bar l_2\vee l_3),\ldots,(\bar l_{s-1}\vee l_s), $$
which correspond to the directed path
$$ l_1\to l_2\to\cdots\to l_s $$
and, after complementation, to the path
$$ \bar l_s\to\bar l_{s-1}\to\cdots\to\bar l_1 . $$
An $s$-snare $(C;t,u)$ adds the clauses in (87), namely
$$ (l_t\vee l_1) $$
and
$$ (\bar l_s\vee l_u) $$
if $u>0$, or
$$ (\bar l_s\vee \bar l_{-u}) $$
if $u<0$.
a)
Suppose that a 2SAT formula $F$ is unsatisfiable. The implication graph characterization of 2SAT says that there is a variable $x$ such that both $x$ and $\bar x$ belong to the same strongly connected component. Hence there are directed paths
$$ x\to\cdots\to\bar x $$
and
$$ \bar x\to\cdots\to x . $$
Choose a shortest directed path from $x$ to $\bar x$, and write it as
$$ l_1\to l_2\to\cdots\to l_s, $$
where $l_1=x$ and $l_s=\bar x$. Because the path is shortest, the literals $l_i$ are distinct, and no two of them are complementary except the endpoints.
The reverse complementary path is
$$ \bar l_s\to\bar l_{s-1}\to\cdots\to\bar l_1 . $$
Since $l_s=\bar l_1$, this path begins at $l_1$ and ends at $\bar l_s$. Therefore the two paths form the standard contradiction cycle
$$ l_1\to l_2\to\cdots\to l_s \quad\text{and}\quad \bar l_s\to\bar l_{s-1}\to\cdots\to\bar l_1 . $$
The first path supplies an $s$-chain $C=(l_1,\ldots,l_s)$. The edge $l_s\to l_1$ is present because the second path reaches $\bar l_1=l_s$, and the chosen path from $\bar l_s$ back to $l_s$ can be shortened until its first repeated literal. Hence there is some index $t$, $1<t\le s$, for which the implication
$$ \bar l_t\to l_1 $$
is present. The corresponding clause is
$$ (l_t\vee l_1). $$
Likewise, the reverse path contains an implication leaving $\bar l_s$ and entering one of the literals among
$$ l_1,l_2,\ldots,l_{s-1}, $$
or their complements. Thus there is an integer $u$ with
$$ 1\le |u|<s $$
such that the formula contains the clause
$$ (\bar l_s\vee l_u) $$
when $u>0$, or
$$ (\bar l_s\vee\bar l_{-u}) $$
when $u<0$.
The clauses of the $s$-chain together with these two additional clauses are precisely the clauses of the snare $(C;t,u)$. Therefore every unsatisfiable 2SAT formula contains all clauses of at least one snare. This completes the proof. ∎
b)
The converse statement is false. The clauses of a snare need not be unsatisfiable.
Consider an $s$-snare built from the chain
$$ C=(l_1,l_2,\ldots,l_s) $$
with the extra clauses
$$ (l_t\vee l_1),\qquad(\bar l_s\vee l_u). $$
Assign
$$ l_1=l_2=\cdots=l_s=1. $$
Every chain clause
$$ (\bar l_i\vee l_{i+1}) $$
is satisfied because $l_{i+1}=1$. The clause
$$ (l_t\vee l_1) $$
is satisfied because both literals are true. The final clause is satisfied because $l_u=1$ when $u>0$, and because the corresponding complementary literal is not forced to be false when $u<0$.
For a concrete example, take $s=3$, $C=(1,2,3)$, $t=2$, and $u=1$. The snare clauses are
$$ (\bar1\vee2),\quad(\bar2\vee3),\quad(2\vee1),\quad(\bar3\vee1). $$
The assignment
$$ 1=2=3=1 $$
satisfies all four clauses. Therefore a snare is not itself necessarily unsatisfiable. This completes the proof. ∎
c)
Let
$$ X(C;t,u)=[\text{all clauses of }(C;t,u)\text{ are present}], $$
as in (88). A fixed $s$-snare contains $s+1$ clauses: the $s-1$ clauses of the $s$-chain and the two additional clauses from (87). The total number of possible binary clauses on $n$ variables is
$$ 2n(n-1), $$
because there are $n(n-1)$ unordered pairs of distinct variables, and two possible sign choices for each pair.
In the random 2SAT model with $m$ independently chosen clauses, the probability that any particular set of $s+1$ clauses appears is at most
$$ \left(\frac{m}{2n(n-1)}\right)^{s+1}. $$
Therefore
$$ \mathop{\rm E}X(C;t,u) \le \left(\frac{m}{2n(n-1)}\right)^{s+1}, $$
which is exactly
$$ \boxed{ \mathop{\rm E}X(C;t,u) \le \frac{m^{s+1}}{(2n(n-1))^{s+1}} }. $$
The inequality holds because the event that all clauses of the snare occur requires the occurrence of each of its $s+1$ specified clauses. This completes the proof. ∎