TAOCP 7.2.2.2 Exercise 279

Exercise 279. [M20] True or false: Every unsatisfiable 2SAT problem has a certificate $(t, \epsilon)$.

Verified: yes
Solve time: 12m23s

Solution

The statement is true.

Let $F$ be an unsatisfiable 2SAT formula. Consider the implication graph of $F$. Each clause $a b$ of $F$ gives the two implications

$$ \bar a\to b,\qquad \bar b\to a . $$

For a 2SAT formula, unit propagation from a literal $l$ derives exactly the literals reachable from $l$ in this implication graph.

Because $F$ is unsatisfiable, the implication graph contains a variable $x$ such that both $x$ and $\bar x$ belong to the same strongly connected component. Hence there are directed paths

$$ x\leadsto\bar x $$

and

$$ \bar x\leadsto x . $$

Choose

$$ t=x . $$

We verify that $(t,\epsilon)$ is a certificate.

For the first certificate condition, we must prove

$$ F\wedge\overline{x}\vdash_1\epsilon . $$

The assumption $\overline{x}$ gives the unit literal $\bar x$. Since

$$ \bar x\leadsto x , $$

unit propagation derives $x$. The formula now contains both unit literals $x$ and $\bar x$, so a contradiction is obtained and

$$ F\wedge\bar x\vdash_1\epsilon . $$

For the second certificate condition, we must prove

$$ F\wedge x\vdash_1\epsilon . $$

The assumption $x$ gives the unit literal $x$. Since

$$ x\leadsto\bar x , $$

unit propagation derives $\bar x$. Again both a literal and its complement are present, so

$$ F\wedge x\vdash_1\epsilon . $$

Therefore the two certificate conditions hold for the sequence

$$ (x,\epsilon). $$

Since every unsatisfiable 2SAT formula has a variable $x$ whose two complementary literals imply each other in the implication graph, every such formula has a certificate of the form $(t,\epsilon)$.

This completes the proof. ∎