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.


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.