Abstract FR:

Le problème de satisfaction de contraintes consiste à exhiber une ou plusieurs solutions d'un système diophantien ou à démontrer la vacuité du domaine associé. La synthèse des differentes implications de ce problème dans le domaine de l'informatique (intelligence artificielle, vectorisation de programmes, vérification de codes, équations sur les mots. . . ) a permis de mettre en évidence les différents modèles typiques de ces applications. L'analyse des techniques de résolution utilisées jusqu'à présent dans le domaine de la vectorisation de programmes a démontré tout l'intérêt de concevoir une nouvelle méthode permettant de trouver efficacement une solution quelque soit l'instance traitée. Cette méthode efficace et robuste appelée fas3t repond aux deux objectifs : preuve de la vacuité du domaine ou de l'existence d'une solution. Les applications à la vectorisation automatique de programmes et au fameux problème de satisfaction d'une expression logique demontrent la rapidité de la méthode fas3t