I have a fully quantified boolean formula in Prenix Normal Form $\Phi = Q_1 x_1, \ldots Q_n x_n . f(x_1, \ldots, x_n)$. As most QBF-Solvers expect $f$ to be in CNF, I use Tseitins Tranformation (Denoted by $TT$). This does not give an equivalent, but an equisatisfiable formula. Which leads to my question:
Does $Q_1 x_1, \ldots Q_n x_n . f(x_1, \ldots, x_n) \equiv Q_1 x_1, \ldots Q_n x_n . TT(f(x_1, \ldots, x_n))$ hold?
To use Tseitin's Transformation for predicate formulas, you'll need to add new predicate symbols of the form $A(x_1, ..., x_n)$. Then the formula $Q_1 x_1, ..., Q_n x_n TT(f(x_1,...,x_n))$ will imply "something" about this new predicate symbols, so the logical equivalence (which I assume what is meant by $\equiv$) does not hold. However $Q_1 x_1 ,..., Q_n x_n TT(f(x_1,...,x_n))$ is a conservative extension of $Q_1 x_1, ..., Q_n x_n f(x_1,...,x_n)$, that is everything provable from $Q_1 x_1, ..., Q_n x_n TT(f(x_1, ..., x_n))$ that does not use the extra symbols is already provable from $Q_1 x_1, ..., Q_n x_n f(x_1, ..., x_n)$
