Oracles for TQBF

Question

I've seen this question somewhere and I've been thinking about it a lot but couldnt think of an answer. Say you have oracles A and B for the TQFB (True Quantified Boolean Formula) decision problem, one being correct and the other one wrong, but you don't know which is which. How do you decide TQFB in polynomial time having access to oracles A and B?

Answer 1

Let $f = Q_1x_1Q_2x_2\dots Q_nx_n\phi(x_1,x_2,\dots,x_n)$, where $Q_i=\exists$ or $Q_i=\forall$ for each $i$. Without loss of generality let us assume that oracle $A$ says that the formula is satisfiable while $B$ says the opposite. The idea behind a polynomial-time algorithm is for each $i$ from 1 to $n - 1$ to get rid of part $Q_ix_i$ and replace $x_i$ in $\phi$ with 0 and then with 1 and query oracles about the modified formulas. There are two cases

1. $Q_i == \exists$. If $A$ says that both modified formulas are unsatisfiable, it does not decide $TQFB$. Similarly if $B$ says that at least one formula is satisfiable, it does not decide $TQFB$.
2. $Q_i == \forall$. If $A$ says that at least one modified formula is unsatisfiable, it does not decide $TQFB$. Likewise if $B$ says that both formulas are satisfiable, it does not decide $TQFB$.

Otherwise there must be at least one formula which is claimed to be satisfiable by $A$ and unsatisfiable by $B$. Let $f$ be that formula and continue. When the formula contains only one variable, we can check its satisfiability in polynomial time. Once we know which oracle decides $TQFB$, we can return its response about the original formula $f$.