Algorithmes d'élimination de quantificateurs pour le calcul des politiques des formules booléennes quantifées

Résumé : Le problème de validité d'une formule booléenne quantifiée est une généralisation du problème de satisfiabilité d'une formule booléenne. Les formules booléennes quantifiées sont utiles pour représenter par exemple des stratégies dans un jeu à deux joueurs mais dans de telles applications c'est une solution au problème de recherche associé qui est nécessaire. La plupart des procédures de décision récentes pour les formules booléennes quantifiées sont des extensions de la procédure de recherche dite de Davis-Putnam et peuvent être aisément étendues au problème de recherche. Ce n'est pas le cas pour les algorithmes basés sur l'élimination de quantificateurs. Dans cet article nous montrons comment des algorithmes d'élimination de quantificateurs peuvent être étendus pour le problème de recherche associé aux formules booléennes quantifiées.