Gestion de la dynamicité et énumération d'impliquants premiers : une approche fondée sur les diagrammes de décision binaire / Fabrice Bouquet ; sous la direction de Philippe Jégou

Thèse de doctorat informatique 1999 Aix-Marseille 1

Cette thèse aborde, d'un point de vue algorithmique, le problème lié aux calculs et à la représentation des modèles d'une formule de la logique propositionnelle. Notre approche est fondée sur les Diagrammes de Décision Binaire (BDD). Ils permettent de représenter facilement l'ensemble des modèles et d'y gérer l'incrémentalité. Le premier travail proposé dans ce mémoire est une étude sur des ordres pour l'insertion de formules particulières de la logique propositionnelle dans un BDD. Pour cela, nous proposons deux actions complémentaires, la première pour réduire la taille du BDD (ordre sur les variables de la formule) et la seconde pour réduire le temps de calcul (stratégie pour l'insertion). Ceci nous a permis de déterminer certaines limites pour l'utilisation des BDD. Dans un second temps, nous proposons d'étendre le formalisme des formules à traiter afin de pouvoir prendre en compte la dynamicité dans les BDD. L'ajout de formules ne posant pas de problème grâce aux BDD, notre extension porte sur le maintien de la cohérence lors de l'ajout ou de la suppression de formules. Nous proposons de résoudre le problème à l'aide d'un codage judicieux et présentons comment appliquer ces travaux dans le cadre des problèmes de satisfaction de contraintes dynamiques. Un impliquant premier peut être vu comme la représentation d'un ensemble de modèles. Une extension naturelle de nos travaux, nous a conduit à élaborer un algorithme de calcul et de gestion des impliquants premiers. Nous montrons ici, comment l'effectuer avec un couplage entre un algorithme énumératif et un BDD. Des expérimentations sont présentées pour illustrer et comparer les différentes approches proposées dans cette thèse