next up previous
suivant: Participants monter: Proposition d'Action Spécifique STIC-CNRS précédent: Plateforme de comparaison expérimentale

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 :


next up previous
suivant: Participants monter: Proposition d'Action Spécifique STIC-CNRS précédent: Plateforme de comparaison expérimentale