Abstract FR:

Cette thèse s'inscrit dans le contexte de la programmation par contraintes sur les domaines finis, un paradigme de programmation qui consiste à exprimer des problèmes combinatoires par le biais de langages formels. L'emploi d'algorithmes de résolution de formules logiques permet ainsi de résoudre une grande variété de problèmes. Les résolveurs de contraintes actuels sont basés sur une logique propositionnelle de laquelle la notion de quantification ("pour tout", "il existe") est absente. Le sujet principal de la thèse est le problème de résolution de contraintes discrètes quantifiées. L'étude de la restriction booléenne de ce problème a récemment fait l'objet d'une intense recherche dans la communauté SAT. A priori, cette restriction n'est cependant pas justifiée et de nombreuses applications s'expriment grâce à une extension du cadre des problèmes de satisfaction de contraintes (CSP) quantifiés ; notre principale contribution est de formuler une technique d'arc-consistance quantifiée, généralisant la technique classique de résolution de CSP. On montre ainsi que l'essentiel du cadre classique de résolution de CSP (notion d'opérateurs de réduction, propriétés de confluence, propagation d'intervalles) peut être adapté à la résolution de problèmes quantifiés. Enfin, nous terminons la thèse en ouvrant une problématique plus prospective : l'utilisation de techniques de compilation logique pour déterminer si les problèmes décrits dans certaines logiques quantifiées peuvent être résolus de manière efficace.