Retour sur trace non chronologique
Dans les algorithmes de recherche et de retour sur trace, le retour sur trace non chronologique ou backjumping est une technique qui réduit l'espace de recherche, et permet donc d'augmenter l'efficacité. En retour sur trace habituel, un retour en arrière remonte d'un niveau dans l'arbre de recherche lorsque toutes les valeurs d'une variable ont été testées. Le retour non chronologique permet de remonter de plusieurs niveaux grâce à une analyse des raisons qui conduisent une combinaison de valeurs pour des variables à échouer. Dans cet article, un ordre fixe de l'évaluation de variables est utilisé, mais les mêmes considérations s'appliquent à une dynamique de l'ordre d'évaluation. Fichier:Backtracking-no-backjumping.svg|Un arbre de recherche visité régulièrement par les retours en arrière Fichier:Backtracking-with-backjumping.svg|Un backjump: le nœud gris n'est pas visité Dans un algorithme de retour sur trace, si pour un nœud de l’arbre de recherche si toutes les valeurs de la variable choisies pour ce nœud conduisent à une contradiction, ou encore si aucune valeur de cette variable ne conduit à une solution, l’algorithme revient alors sur la valeur de la variable du nœud parent en tentant une nouvelle valeur, puis à la valeur de la précédente variable si de même toutes les valeurs ont été essayées. Si est l’affectation partielle courante des variables et si toutes les valeurs de ont été essayées sans trouver une solution, l’algorithme conclut qu'aucune pour les valeurs n’existe. Alors l'algorithme « remonte » à , et choisit si possible une nouvelle valeur à affecter à , ou bien retourne de nouveau en arrière s'il n’y a plus de valeur à essayer. Toutes les valeurs de l’affectation partielle ne sont pas toujours nécessaires pour démontrer qu’aucune valeur de ne permet d'aboutir à une solution. En particulier, un préfixe de l’affectation partielle peut avoir la même propriété, c’est-à-dire qu’il existe un indice tel que ne peut pas être étendue pour former une solution quelle que soit la valeur de .
