Compilation des QCSP

Nous proposons dans cet article un cadre formel pour la compilation des problèmes de satisfaction de contraintes quantifiées (QCSP). L\u27objectif d\u27une telle compilation est de répondre au problème du choix du prochain mouvement de manière polynomiale en temps même lorsque la solution courante n\u27est plus accessible. Nous établissons la sémantique de ce formalisme en terme d\u27interprétation en un QCSP. Nous en étudions les propriétés en particulier vis-à-vis du QCSP compilé. Nous spécifions deux algorithmes de compilation basés sur un algorithme de recherche. Le premier est imbriqué dans l\u27algorithme de recherche et reprend la structure inductive de la sémantique des QCSP ; le second est un analyseur de trace d\u27exécution d\u27un solveur QCSP