Decidabilite et complexite de systemes de contraintes ensemblistes
Institution:
BesançonDisciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
Les resultats de recherche presentes dans cette these concernent l'etude de la decidabilite et de la complexite du probleme de satisfiabilite d'un systeme de contraintes ensemblistes. Cette these est composee de deux parties. Dans la premiere nous etudions le probleme de satisfiabilite des contraintes ensemblistes dans un univers heterogene d'ensembles hereditairement finis. Nous donnons certains resultats de complexite qui montrent 1) le caractere np-dur du probleme en question meme pour un fragment tres reduit, 2) le caractere np pour les fragments etudies, en utilisant des techniques connues mais avec une nette amelioration de la complexite calculatoire. Nous proposons ensuite deux approches pour resoudre le probleme de satisfiabilite. La premiere est basee sur une reduction polynomiale du probleme de satisfiabilite des formules ensemblistes a sat. La deuxieme est une reduction du probleme de satisfiabilite pour les formules conjonctives a un probleme equivalent de programmation lineaire en entiers. La deuxieme partie de la these consiste en l'etude du probleme de satisfiabilite de contraintes sur ensembles, multi-ensembles et sequences. Ces contraintes sont etablies dans le cadre d'un univers d'objets homogenes regroupant les trois structures avec des imbrications hereditaires et finies. Nous montrons qu'a partir d'un typage partiel des operateurs utilises on peut determiner modulo des types minimaux tous les objets apparaissant dans un systeme de contraintes sur ensembles, multi-ensembles et sequences. Ceci nous permet de montrer la decidabilite des systemes en question. Nous montrons que le probleme est np-complet, et generalisons la reduction en un probleme de programmation lineaire en entiers avec une amelioration du cout de complexite calculatoire de la reduction. Nous donnons a la fin quelques applications, notamment un environnement pour la reduction en programmation lineaire ainsi qu'un schema d'integration de celle-ci dans le langage clps