Dans un premier temps, il est envisagé de recenser et d'évaluer les démonstrateurs QBF existants. Ceci nécessite de définir des critères de comparaison adaptés. Quel type de problème est traité ? S'agit-il du problème de décision, d'un problème de recherche de solution, d'optimisation, ou encore (s'il n'existe pas de solution) d'approximation ? S'il s'agit d'un problème de recherche, faut-il demander un certificat (i.e. une preuve de validité) pour toute solution trouvée par un démonstrateur QBF ? Si, pour le problème SAT, la taille d'un tel certificat (correspondant par exemple à un modèle) est linéaire dans la taille de l'entrée, pour le problème UNSAT, on ne connait pas de certificats de taille polynomiale. Le fait de monter dans la hiérarchie polynomiale ne peut que compliquer la tâche et pose clairement des problèmes de représentation des certificats. La possibilité de les comparer est également cruciale, tant pour le recoupement et la comparaison des résultats de différents démonstrateurs que pour aborder des problèmes d'optimisation.