Decidability of equivalence to existential formulas
Surely, no such algorithm can exist in the general case: for a statement of the form $\forall x.\varphi$ statement in arithmetic, with $\varphi$ quantifier-free, there is a $\exists y.\psi$ statement such that

$$ \forall x.\varphi\ \Leftrightarrow \exists y.\psi$$

if and only if the statement is $\Delta_0$, aka decidable. Because $\forall$ statements are undecidable in general, such an algorithm cannot exist.



Edit: The above reasoning is wrong! Indeed, the Bernays-Shönfinkel class of formulas includes the set of $\forall^*\exists^*$ formulas without function symbols (but with arbitrary relational symbols) and is decidable. The $\Delta_0$ statements of arithmetic are not strictly speaking, quantifier free, but only contain bounded quantifiers (which are still quantifiers in FOL!)

However, this suggests an alternate proof: if there were a decision procedure which decides whether an arbitrary sentence were equivalent to some $\exists^*$ sentence, then there would be a decision procedure for arbitrary (function-free) formulas as follows:

Given $\phi$ check whether it is equivalent to an existential formula $\psi$. If it is not, $\phi$ is not provable (otherwise it would be equivalent to the formula $\exists x.\top$).

If it is, then find such a $\psi$ (it's easy to show this is possible) and apply the decision procedure for the B-S class.



Finally, an exercise: repair the above proof using the undecidability of arithmetic.