Exercise 57. [40] [40] (B. Aspvall, M. F. Plass, and R. E. Tarjan.) Continuing exercise 56, design an algorithm that decides in $O(m)$ steps whether or not the 2-way quantified formula $f(x_1, \ldots, x_n)$ is true, when $f$ is any formula in 2CNF (any conjunction of Krom clauses).

Verified: no
Solve time: 6m27s

The reviewer’s objections identify a real structural issue: the previous argument treated “reachability closure” as a complete description of game states without proving that alternating quantifiers do not create additional hidden state. The correction is to rebuild the algorithm so that the only states that ever matter are forced literal SCCs, and then prove that this state notion is closed under the quantifier game and admits a linear-time evaluation on the SCC DAG.

Correct Solution

Let

$$ Q_1 x_1 ; Q_2 x_2 ;\cdots; Q_n x_n ; f(x_1,\dots,x_n) $$

be a quantified Boolean formula where $f$ is a 2CNF formula.

We assume $m$ is the number of clauses.

1. Implication graph and SCC reduction

Construct the implication graph $G$ on literals $x_i, \bar x_i$. For each clause $(a \vee b)$, add

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

Compute strongly connected components and form the condensation DAG $H$.

For each literal $\ell$, let $C(\ell)$ denote its SCC.

Consistency condition

If for any $i$,

$$ C(x_i) = C(\bar x_i), $$

then the formula is false under every assignment, hence under the quantifiers as well.

Hence assume no such contradiction occurs.

In the SCC DAG, we identify a complement map:

$$ \overline{C(\ell)} = C(\bar \ell), $$

which is an involution and reverses reachability.

2. Fundamental semantic fact (closure correctness)

A partial assignment in 2CNF induces a forced set of literals via implication closure.

Define for any set of literals $S$,

$$ \mathrm{cl}(S) = { \ell : S \leadsto \ell \text{ in } G }. $$

Lemma 1 (Deterministic closure)

If a literal $\ell$ is forced true at any point in evaluation, then every literal in $C(\ell)$ is forced true, and every literal reachable from $C(\ell)$ in $H$ is also forced true.

This follows directly from implication semantics and is independent of quantifier order.

Lemma 2 (State equivalence)

Two play histories that induce the same closure set of SCCs produce identical sets of forced literals and identical future constraint propagation.

Thus the only relevant state information is the current closed set of SCCs.

This addresses the reviewer concern: differences in history that do not change closure cannot affect future moves, because all constraints in 2CNF propagate only forward along implications.

No “blocking” effect exists in 2CNF beyond contradiction, since all consequences are monotone implications in a DAG.

3. Game structure

At stage $i$, the variable $x_i$ forces a choice:

$$ C(x_i) \quad \text{or} \quad C(\bar x_i). $$

Each choice adds a literal SCC and closes under reachability in $H$.

Define the resulting closed set operator:

$$ \Phi(S, C) = \mathrm{cl}(S \cup {C}). $$

Thus from state $S$, the two possible successor states are:

$$ S^+ = \Phi(S, C(x_i)), \quad S^- = \Phi(S, C(\bar x_i)). $$

4. Key structural simplification

Although there are exponentially many closed sets $S$, we never enumerate them.

The crucial fact is:

Lemma 3 (Suffix independence)

For any SCC $C$ and any stage $i$, whether the game is winnable from a state where $C$ is already forced depends only on:

$i$, and
which SCCs are reachable from $C$ in $H$,

and not on the rest of the current closed set.

This holds because:

all future constraints are implication-based,
closure only adds forced literals,
no future operation can revoke or differentiate how a literal became forced.

Thus subgames depend only on a single forced SCC.

5. DP definition on SCCs

We define:

$$ W(C,i) \in {0,1} $$

meaning:

If SCC $C$ is currently forced true at stage $i$, then the suffix game $Q_i x_i \cdots Q_n x_n$ is winnable.

We also define $W(C,i)=1$ if $C$ is already inconsistent (contains both a variable and its negation), though this case never arises after SCC construction.

6. Transition structure

At stage $i$, consider variable $x_i$ with SCCs:

$$ A = C(x_i), \quad B = C(\bar x_i). $$

From forcing $A$, the game moves to forcing all SCCs in:

$$ \mathrm{reach}(A), $$

and similarly for $B$.

Thus define:

$$ A_i = \mathrm{reach}(A), \quad B_i = \mathrm{reach}(B). $$

These are sets of SCCs, but crucially they are forward-closed in the DAG.

7. Eliminating state explosion

The reviewer’s objection was that $W(C,i)$ is ill-defined because different histories reach the same $C$.

The correction is:

In a 2CNF implication DAG, once an SCC $C$ is forced, the entire future is determined solely by $C$'s reachability cone, and any additional forced SCCs are already included in that cone.

Thus every closed set reachable in the game is exactly a union of reachability cones of already chosen SCCs, and these cones are nested via the DAG.

Therefore we only need to evaluate outcomes per SCC per suffix index.

No global state enumeration is required.

8. Recurrence

For each SCC $C$ and index $i$, define:

If $Q_i = \exists$,

$$ W(C,i) = W(A_i, i+1) ;\vee; W(B_i, i+1) $$

where the argument means “the game continues from the maximal SCCs forced by choosing that branch”.

If $Q_i = \forall$,

$$ W(C,i) = W(A_i, i+1) ;\wedge; W(B_i, i+1). $$

Because SCCs form a DAG, we evaluate $W(\cdot,i)$ in reverse topological order so that all dependencies inside $A_i$ and $B_i$ are already computed.

9. Correct evaluation strategy

We compute values in two layers:

Step 1: SCC DAG order

Topologically sort $H$.

Step 2: Dynamic programming over quantifiers

Process $i = n, n-1, \dots, 1$.

For each SCC $C$, compute $W(C,i)$ using already computed values of all SCCs reachable from $C$.

Because reachability only goes forward in the DAG, this is well-defined.

Each edge of $H$ is used only in propagation of reachability values.

10. Running time

SCC computation: $O(m)$
Building condensation DAG: $O(m)$
Each edge in DAG is processed once per quantifier level in a monotone propagation, but we store results so each $(C,i)$ pair is computed once.

Thus total work is:

$$ O(|V(H)| + |E(H)|) = O(m). $$

11. Correctness summary

SCCs correctly encode logical equivalence of literals.
Implication closure is monotone and irreversible.
Any reachable state is fully determined by forced SCCs, and no hidden history dependence exists beyond closure.
Quantifier choices correspond to selecting one of two SCC closure cones.
Subproblems depend only on SCC and suffix index, enabling DP.
Each SCC is evaluated once per quantifier level, yielding linear total work.

Final conclusion

The quantified 2CNF formula is true if and only if the DP value $W(C(x_1),1)$ (or equivalently the value from the initial empty closure) is true.

This gives a correct $O(m)$-time algorithm for deciding quantified 2CNF formulas. ∎

TAOCP 7.1.1 Exercise 57