Trouver un modèle

let trouve_modele f =
  let n = nb_variables f in
  let v = Array.make n false in
  let rec essaie i =
    if i = n then (if evalue v f then Some (Array.copy v) else None)
    else begin
      v.(i) <- false;
      match essaie (i + 1) with
      | Some m -> Some m
      | None -> v.(i) <- true; essaie (i + 1)
    end
  in
  essaie 0

C'est satisfiable qui, au lieu de renvoyer true, rapporte la valuation trouvée — d'où le Array.copy v (chapitre 5) pour figer une copie indépendante de v (qui, mutable, continue d'évoluer). C'est le squelette d'un solveur SAT : explorer, et reconstruire la solution le long des choix réussis (chapitre 11).