How 2-QCNF algorithm works?

Question

Suppose we have following 2-QCNF problem:

$$\forall x_1...\forall x_m\exists y_1...\exists y_k:\varphi(x_1,...,y_k)$$

where $\varphi$ is 2-CNF.

When the formula is false?

Rules that I found:

1. $\exists y_i:(y_i\rightarrow \overline{y_i})\land(\overline{y_i}\rightarrow y_i).$ Existentially quantified variable and it's negation are strongly connected.
2. $\exists\{x_i,x_j\}:(x_i\rightarrow x_j)\lor(\overline{x_i}\rightarrow x_j)\lor(x_i\rightarrow \overline{x_j})\lor(\overline{x_i}\rightarrow \overline{x_j}).$ Two (or one and it's negation) totally quantified variables are connected.
3. $\exists\{x_i,y_j\}:((y_j\rightarrow x_i)\land(\overline{y_j}\rightarrow x_i))\lor((y_j\rightarrow \overline{x_i})\land(\overline{y_j}\rightarrow \overline{x_i})).$ Totally quantified variable is reachable from existentially quantified variable and it's negation.

Is there any other rule to solve 2-QCNF or, maybe, there is better way to solve it?

Answer 1

Aspvall, Plass and Tarjan describe a linear time algorithm determining the truth value of quantified 2CNFs in their paper A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Their algorithm is an extension of the well-known algorithm for solving 2SAT using directed reachability; their initial step is computing the strongly connected components of the implication graph.