Résolution de problèmes combinatoires modélisés par des contraintes quantifiées

Cette these s'inscrit dans le contexte de la programmation par contraintes sur les domaines finis, un paradigme de programmation qui consiste a exprimer des problemes combinatoires par le biais de langages formels. L'emploi d'algorithmes de resolution de formules logiques permet ainsi de resoudre une grande variete de problemes. Les resolveurs de contraintes actuels sont bases sur une logique propositionnelle de laquelle la notion de quantification ("pour tout", "il existe") est absente. Le sujet principal de la these est le probleme de resolution de contraintes discretes quantifiees. L'etude de la restriction booleenne de ce probleme a recemment fait l'objet d'une intense recherche dans la communaute SAT. A priori, cette restriction n'est cependant pas justifiee et de nombreuses applications s'expriment grâce a une extension du cadre des problemes de satisfaction de contraintes (CSP) quantifies ; notre principale contribution est de formuler une technique d'arc-consistance quantifiee, generalisant la technique classique de resolution de CSP. On montre ainsi que l'essentiel du cadre classique de resolution de CSP (notion d'operateurs de reduction, proprietes de confluence, propagation d'intervalles) peut etre adapte a la resolution de problemes quantifies. Enfin, nous terminons la these en ouvrant une problematique plus prospective : l'utilisation de techniques de compilation logique pour determiner si les problemes decrits dans certaines logiques quantifiees peuvent etre resolus de maniere efficace.