Correctness of following algorithm for 3-QCNF?

Let I have 3-QCNF formula.

Classic recursive algorithm for TQBF takes exponential time. However, following divide & 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?

• 1. Are the $f_i$ literals, or more complex formulas? If $f_i$'s are formulas, then $\Phi$ is not a 2-SAT formula. Do you mean that each $f_i$ is itself a 2-CNF formula? 2. What do you mean by "number of subformulae is inversely proportional to their length", and what is the justification for that statement? And why is that relevant? 3. What do you mean by "solved"? Are you asking about a polynomial-time algorithm to test whether $\Phi$ is satisfiable? If so, what have you tried? Have you tried to reduce from 3-SAT (or, in this case, from 4-SAT)? – D.W. Jun 21 '17 at 3:48
• @D.W. Well, I have generalized the question. Yes, it was reduction from 3-SAT, but the question is if I can use divide & conquer techniques. – rus9384 Jun 21 '17 at 10:36
• Your algorithm is very likely incorrect. You can try programming it and finding a counterexample by comparing to a brute-force algorithm. – Yuval Filmus Jun 21 '17 at 15:56
• @YuvalFilmus, okay, it really doesn't work, I need to make subformulae for all variables as well as adding low-order conjunction. All of this seems to be quite hard. – rus9384 Jun 22 '17 at 7:58

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.
• But where I have messed with quantification? If $x_1$ is $\forall$-quantified, algorithm doesn't choose it. – rus9384 Jun 21 '17 at 18:24