1
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ 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)? $\endgroup$
    – D.W. ♦
    Jun 21, 2017 at 3:48
  • $\begingroup$ @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. $\endgroup$
    – rus9384
    Jun 21, 2017 at 10:36
  • 1
    $\begingroup$ Your algorithm is very likely incorrect. You can try programming it and finding a counterexample by comparing to a brute-force algorithm. $\endgroup$
    – Yuval Filmus
    Jun 21, 2017 at 15:56
  • $\begingroup$ @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. $\endgroup$
    – rus9384
    Jun 22, 2017 at 7:58

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ But where I have messed with quantification? If $x_1$ is $\forall$-quantified, algorithm doesn't choose it. $\endgroup$
    – rus9384
    Jun 21, 2017 at 18:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.