QBF Solvers

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.

Based on QDPLL, with conflict-driven clause and solution-driven cube learning.
link open source

DPLL-based solver that uses ghost variables to achieve symmetry in handling of universal/existential variables.
link open source 

Based on recursively using counterexample abstraction refinement (CEGAR).
link open source 

For more on QBF solvers, see QBFLIB and the QBF Gallery.