Nous proposons dans cet article un cadre formel pour la compilation des problèmes de satisfaction de contraintes quantifiées (QCSP). L'objectif d'une 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'est plus accessible. Nous établissons la sémantique de ce formalisme en terme d'interpré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'algorithme de recherche et reprend la structure inductive de la sémantique des QCSP ; le second est un analyseur de trace d'exécution d'un solveur QCSP.
