# 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, 2017 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. Jun 21, 2017 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. Jun 21, 2017 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. Jun 22, 2017 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. Jun 21, 2017 at 18:24