Checking formulas with two quantifiers ($\forall \exists$) - 2QBF SAT solvers give a powerful way to check the validity of a boolean formula with one quantifier.

For instance, to check the validity of $\exists x . \varphi(x)$, we can use a SAT solver to determine whether $\varphi(x)$ is satisfiable.  To check the validity of $\forall x . \varphi(x)$, we can use a SAT solver to determine whether $\neg \varphi(x)$ is satisfiable.  (Here $x=(x_1,\dots,x_n)$ is a $n$-vector of boolean variables, and $\varphi$ is a boolean formula.)

QBF solvers are designed to check the validity of a boolean formula with an arbitrary number of quantifiers.

What if we have a formula with two quantifiers?  Are they any efficient algorithms for checking validity: ones  that are better than just using generic algorithms for QBF?  To be more specific I have a formula of the form $\forall x . \exists y . \psi(x,y)$ (or $\exists x . \forall y . \psi(x,y)$), and want to check its validity.  Are there any good algorithms for this?  Edit 4/8: I learned that this class of formulas is sometimes known as 2QBF, so I am looking for good algorithms for 2QBF.

Specializing further: In my particular case, I have a formula of the form $\forall x . \exists y . f(x)=g(y)$ whose validity I want to check, where $f,g$ are functions that produce a $k$-bit output.  Are there any algorithms for checking the validity of this particular sort of formula, more efficiently than generic algorithms for QBF?

P.S. I am not asking about the worst-case hardness, in complexity theory.  I am  asking about practically useful algorithms (much as modern SAT solvers are practically useful on many problems even though SAT is NP-complete).
If I may, quite blatantly, advertise myself, we wrote an article about this last year
Abstraction-Based Algorithm for 2QBF. I've got an implementation for qdimacs, which I can provide if you wish but from my experience, one can benefit greatly from specializing the algorithm for a particular problem. There is also an older paper A Comparative Study of 2QBF Algorithms, which also presents fairly easily implemetable algorithms.