QBF solvers can applied to problems in the Polynomial Hierarchy (PH). Often, problems are specified via quantified CNF formulas, although a number of other formats exist.
DepQBF
Based on QDPLL, with conflict-driven clause and solution-driven cube learning.
link open source
GhostQ
DPLL-based solver that uses ghost variables to achieve symmetry in handling of universal/existential variables.
link open source
RAReQS
Based on recursively using counterexample abstraction refinement (CEGAR).
link open source
For more on QBF solvers, see QBFLIB and the QBF Gallery.