Conclusion

Les progrès considérables réalisés autour du problème SAT sont dûs à une meilleure connaissance des performances pratiques des algorithmes, grâce notamment à l'organisation de compétitions et de véritables études expérimentales de ces algorithmes (études d'une importance encore rare dans bien d'autres domaines de la démonstration automatique). Aujourd'hui, toute une partie de la communauté SAT se tourne vers le problème QBF, d'où viennent la plupart des problèmes actuels. Cette action lie ces deux domaines encore émergeants, c'est-à-dire le développement d'algorithmes QBF conjointement à leur évaluation (au travers par exemple d'un site web dédié à leur comparaison expérimentale), ce qui constitue certainement un challenge important pour la démonstration automatique dans les années à venir. En résumé, les objectifs de cette action sont :

• d'identifier les spécificités de l'évaluation de démonstrateurs QBF ;

• d'évaluer les démonstrateurs QBF existants (sur la base d'une publication web des résultats, et grâce à une plateforme d'expérimentation, sur le modèle SAT-EX).

• d'obtenir une meilleure connaissance du domaine pratique de la résolution des QBF, par exemple en étudiant la pertinence des formules aléatoires et en proposant un regroupement des problèmes et démonstrateurs en familles (sur la base des résultats expérimentaux) ;

• de tirer parti de cette évaluation pour étudier de nouveaux axes ou proposer des améliorations des méthodes existantes.