Problème — Le sudoku : la même exploration, deux ordres de choix

1. Le solveur lexicographique.

(* Vrai si la grille g admet un remplissage ; g est alors modifiée en place et
   contient une solution. Précondition : g est un tableau 9 x 9, 0 = case vide,
   et les chiffres déjà posés respectent les règles. *)
let admissible g i j v =
  let ok = ref true in
  for k = 0 to 8 do
    if g.(i).(k) = v || g.(k).(j) = v then ok := false
  done;
  let bi = 3 * (i / 3) and bj = 3 * (j / 3) in
  for a = 0 to 2 do for b = 0 to 2 do
    if g.(bi + a).(bj + b) = v then ok := false done done;
  !ok

let resoudre g =
  let rec explorer k =
    if k = 81 then true
    else
      let i = k / 9 and j = k mod 9 in
      if g.(i).(j) <> 0 then explorer (k + 1)     (* case donnée : on passe *)
      else begin
        let fini = ref false and v = ref 1 in
        while not !fini && !v <= 9 do
          if admissible g i j !v then begin
            g.(i).(j) <- !v;
            if explorer (k + 1) then fini := true
            else g.(i).(j) <- 0                   (* on DÉFAIT *)
          end;
          incr v
        done;
        !fini
      end
  in explorer 0

Terminaison : variant $81-k$, qui décroît strictement à chaque appel récursif. Correction : à tout instant la grille est partiellement valide — l'appel n'est fait qu'après un test admissible —, et l'on n'atteint $k=81$ qu'avec les $81$ cases remplies, donc avec une solution.