suivant: Participants
monter: Proposition d'Action Spécifique STIC-CNRS
précédent: Plateforme de comparaison expérimentale
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.
suivant: Participants
monter: Proposition d'Action Spécifique STIC-CNRS
précédent: Plateforme de comparaison expérimentale