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).
Checking formulas with two quantifiers ($\forall \exists$) - 2QBF
ds.algorithms;lo.logic;sat;boolean functions