Compter les chemins hamiltoniens, avec la grille complète

(* Nombre de chemins hamiltoniens de g partant du sommet depart.
   Précondition : g est une matrice d'adjacence n x n, 0 <= depart < n.
   Postcondition : le résultat est compris entre 0 et (n-1)!.
   Complexité : O(n!) au pire, O(n) en espace (le tableau vu et la pile). *)
let chemins_hamiltoniens g depart =
  let n = Array.length g in
  let vu = Array.make n false in
  let total = ref 0 in
  (* INVARIANT : vu.(s) est vrai exactement pour les sommets du chemin courant,
     lequel compte k sommets et finit en courant. *)
  let rec explorer courant k =
    if k = n then incr total
    else
      for s = 0 to n - 1 do
        if g.(courant).(s) && not vu.(s) then begin
          vu.(s) <- true;
          explorer s (k + 1);
          vu.(s) <- false                 (* on DÉFAIT *)
        end
      done
  in
  vu.(depart) <- true;
  explorer depart 1;
  !total

Terminaison. Variant : $n-k$, le nombre de sommets restant à visiter. Chaque appel récursif se fait avec $k+1$, donc le variant décroît strictement de $1$ et reste positif ou nul. La profondeur est bornée par $n$.

Correction. L'invariant est rétabli à chaque retour par la ligne qui défait : sans elle, $\mathtt{vu}$ ne décrirait plus le chemin courant mais l'union de tous les chemins déjà essayés, et le compte serait faux — c'est exactement l'exercice 14.3. À la sortie, on a compté une fois chaque suite de $n$ sommets deux à deux distincts, reliés consécutivement, commençant en depart : c'est la définition d'un chemin hamiltonien.

Complexité. L'arbre de recherche a au plus $(n-1)!$ feuilles : à chaque étage, un sommet de moins est disponible. Sur un graphe complet, cette borne est atteinte. Le graphe complet à $9$ sommets a donc $8!=40320$ chemins hamiltoniens depuis un sommet donné, et son arbre de recherche compte $109601$ nœuds — mesuré au problème 14.5.

Et il n'y a pas mieux. Décider si un graphe possède un chemin hamiltonien est np-complet (chapitre chap:decidabilite). Le retour sur trace n'est donc pas un pis-aller : c'est, à ce jour, ce que l'on sait faire.