Checking formulas with two quantifiers ($\forall \exists$) - 2QBF
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.