Domaines de congruence pour la programmation par contraintes

Résumé : Dans un système de Programmation par Contraintes (PPC), une \emph{convergence lente} se produit lorsque la propagation prend un temps proportionnel à la taille des domaines des variables. Ce phénomène survient par exemple sur des équations entières aussi simples que $x = 2y + 1$ et $x = 2z$. Les contraintes qui interviennent dans l'analyse de programmes portent souvent sur des variables dont les domaines s'étendent à tous les entiers représentables en machine. Dans ce cas, la convergence lente empêchera en pratique d'atteindre le point fixe de réduction des domaines. Pour lutter contre ce phénomène de convergence lente, nous proposons d'utiliser les \emph{domaines de congruence} pour enrichir les domaines de la PPC. Cette id ée a été introduite par Ph. Granger~\cite{Granger89} dans la communauté de l'interprétation abstraite; nous montrons ici comment un système de PPC peut en tirer parti, par exemple pour découvrir que $12x + |y| = 3$ et $4x + 7y = 0$ n'ont pas de solution entière.