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. ∎