Une nouvelle stratégie de mise sous forme prénexe pour des formules booléennes quantifiées avec bi-implications

La plupart des procédures pour résoudre le problème de validitédes formules booléennes quantifiées prennent en entrée seulement des formules sous forme normale négative, voire sous forme normale conjonctive, et donc prénexes. Mais, il est rarement naturel d’exprimer un problème directement sous cette forme. Par exemple, en spécification, des symboles propositionnels existentiellement quantifiés sont insérés, selon un même motif, pour capturer des résultats intermédiaires. Ainsi, pour pouvoir utiliser les solveurs de l’état de l’art, il est nécessaire de convertir toute formule booléenne quantifiée sous forme prénexe. Un problème majeur de cette mise sous forme prénexe est qu’elle détruit complètement la structure originale de la formule. De plus, lors de la mise sous forme prénexe des bi-implications il y a duplication de leurs sous-formules, ceci incluant les quantificateurs. Cela conduit généralement à une croissance exponentielle de la taille de la formule. Dans ce travail, nous nous focalisons sur le motif très courant des résultats intermédiaires. Nous mettons en évidence des équivalences logiques qui permettent d’extraire les sous-formules améliorant ainsi nettement les performances des solveurs de l’état de l’art