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).