Correctness of following algorithm for 3-QCNF? Let I have 3-QCNF formula.

Classic recursive algorithm for TQBF takes exponential time. However, following divide &amp; conquer modification allows to do it in quadratic time (not sure about correctness, and that's the question).

ctr = 0

for i = 0..n

    Step 1. Take i'th clause, find E-quantified variable inside it. 
    If can't, return 'NO'. Otherwise, if it's the clause containing 3 
    variables, choose that variable v.

    Step 2. Find all 3-clauses with variable v. Move them from formula Ф
    to formula f_i. Reduce n (length of formula Ф) by number of moved 
    clauses.

    Step 3. Copy f_i to f'_i.

    Step 4. Put v = 1 in f_i. Get 2-QCNF.

    Step 5. Put v = 0 in f'_i. Get 2-QCNF.

    Step 6. If f_i and f'_i have same clauses, move them to Ф.
    Increase n by number of moved clauses.

    Step 7. ctr = ctr + 1

for i = 0..ctr

    Step 1. Solve 2-QCNF Ф'^f_i. //Ф' is changed Ф.

    Step 2. Solve 2-QCNF Ф'^f'_i.

    Step 3. If both are false, return 'NO'.

return 'YES'


Notes:

Algorithm represents 3-QCNF as $\mathsf{\Phi = TAUT-CNF \land \Phi'(2-QCNF) \land (f_i(2-QCNF) \lor f'_i(2-QCNF))\land\ ..}$

Trivially, formula is false if TAUT-CNF contains clauses.

So, if TAUT-CNF has no clauses, formula is represented this way:

$\mathsf{\Phi' \land (f_i \lor f'_i)\land\ ...\ =((\Phi'\land f_i)\lor(\Phi'\land f'_i))\land\ ...}$

The question: have I violated any logical rule in my algorithm?
Your code ignores quantification levels.  Formulas prefixed with
$\exists{x_1}\forall{x_2}$ are not supposed to be evaluated the same way as those prefixed with $\forall{x_1}\exists{x_2}$.  Your code treats them the same, moving one existential quantifier ahead of all the other quantifiers in each of your 2-QBF subformulas.