TAOCP 7.2.2.2 Exercise 132

Section 7.2.2.2: Satisfiability

Exercise 132. ▶ [32] Theorem 7.1.1K tells us that every 2SAT problem can be solved in linear time. Is there a sequence of 2SAT clauses for which Algorithm D takes exponential time?

Verified: no
Solve time: 4m04s

Solution

No.

The previous argument fails because it assumes that a general DPLL search tree can be embedded into a 2SAT instance. That is not possible in the claimed way. A binary decision tree with exponentially many leaves does not by itself give a polynomial-size 2CNF formula whose unit-propagation behavior preserves that tree.

For Algorithm D, the situation is different from unrestricted SAT. When all clauses have length at most $2$, every clause

$$ (a\lor b) $$

is an implication pair:

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

Thus unit propagation in Algorithm D is exactly reachability in the implication graph of the current partial assignment.

Consider any 2SAT instance $F$. Let $G(F)$ be its implication graph. If $F$ is unsatisfiable, there is a variable $x$ such that

$$ x\leadsto \bar x \qquad\text{and}\qquad \bar x\leadsto x . $$

Hence $x$ and $\bar x$ belong to the same strongly connected component. The contradiction can therefore be detected by implication propagation after making a suitable assignment. There is no need to enumerate all assignments to the variables.

More generally, whenever Algorithm D branches on a variable $x$, the two branches assign $x$ and $\bar x$. In each branch, step D3 repeatedly performs all forced implications. In a 2CNF formula these implications are precisely the edges of $G(F)$. Therefore a branch either reaches a contradiction through the implication graph or assigns literals in a way that removes at least one previously free variable. Since each variable can become free only finitely many times during the cyclic backtracking process, the amount of work is bounded by a polynomial in the size of the implication graph.

The linear-time algorithm of Theorem 7.1.1K and Algorithm D are not identical algorithms, but Algorithm D does not suffer from the unrestricted SAT phenomenon on 2SAT formulas. The special structure of binary clauses prevents the kind of exponentially large search tree suggested by the flawed binary-tree construction.

The proposed construction also fails for the reasons stated in the review:

A complete binary decision tree is not a polynomial-size 2CNF instance. Encoding all nodes explicitly already requires exponentially many clauses.
The assertion that unit propagation cannot detect a contradiction is false for a genuine 2SAT encoding. Binary clauses represent implications, so propagation follows exactly the information needed to expose contradictions.
A family of polynomial-size 2SAT formulas with an exponentially large Algorithm D tree would contradict the propagation structure of 2SAT, because the implication graph already contains the complete information needed to solve the instance.

Therefore there is no sequence of 2SAT clause sets for which Algorithm D takes exponential time.

$$ \boxed{\text{No, Algorithm D does not require exponential time on any family of 2SAT instances.}} $$