Logique propositionnelle

let v = [| false; false; true |]
(* evalue v f : Ou (false, not false) = Ou(false, true) = true ; Et(true, true) = true *)

evalue v f vaut true : Var 0 est false, Non (Var 1) est true, leur ou est true ; Var 2 est true ; le et final est true.

let rec var_max f =
  match f with
  | Var i -> i
  | Non g -> var_max g
  | Et (g, h) | Ou (g, h) ->
      let a = var_max g and b = var_max h in if a >= b then a else b

let nb_variables f = var_max f + 1

La plus grande variable de f est Var 2, donc nb_variables f = 3. On suppose les variables numérotées sans trou de 0 à n-1.

let rec taille f =
  match f with
  | Var _ -> 1
  | Non g -> 1 + taille g
  | Et (g, h) | Ou (g, h) -> 1 + taille g + taille h

Récursion sur l'arbre : une feuille compte 1, un connecteur unaire 1 + sa sous-formule, un binaire 1 + les deux. C'est la fonction taille des arbres du chapitre 3, adaptée.

let satisfiable f =
  let n = nb_variables f in
  let v = Array.make n false in
  let rec essaie i =
    if i = n then evalue v f
    else begin
      v.(i) <- false;
      if essaie (i + 1) then true
      else begin v.(i) <- true; essaie (i + 1) end
    end
  in
  essaie 0

satisfiable (Et (Var 0, Non (Var 0))) vaut false : aucune valuation ne rend x0 et not x0 simultanément vrais — c'est une contradiction.

let tautologie f =
  let n = nb_variables f in
  let v = Array.make n false in
  let rec essaie i =
    if i = n then evalue v f
    else begin
      v.(i) <- false;
      essaie (i + 1) && (v.(i) <- true; essaie (i + 1))
    end
  in
  essaie 0

Toute valuation doit rendre la formule vraie : le && exige les deux branches (x_i faux et vrai) et s'arrête au premier échec. tautologie (Ou (Var 0, Non (Var 0))) vaut true. On a aussi tautologie f = not (satisfiable (Non f)).

let nb_modeles f =
  let n = nb_variables f in
  let v = Array.make n false in
  let rec compte i =
    if i = n then (if evalue v f then 1 else 0)
    else begin
      v.(i) <- false;
      let a = compte (i + 1) in
      v.(i) <- true;
      a + compte (i + 1)
    end
  in
  compte 0

On parcourt l'arbre des $2^n$ valuations en additionnant les contributions (comme le comptage de sous-ensembles du chapitre 11), au lieu de s'arrêter à la première. Une tautologie a $2^n$ modèles, une contradiction $0$.

let equivalentes f g =
  let n =
    let a = var_max f and b = var_max g in (if a >= b then a else b) + 1
  in
  let v = Array.make n false in
  let rec verifie i =
    if i = n then evalue v f = evalue v g
    else begin
      v.(i) <- false;
      verifie (i + 1) && (v.(i) <- true; verifie (i + 1))
    end
  in
  verifie 0

On prend le nombre de variables couvrant les deux formules, puis on vérifie l'égalité evalue v f = evalue v g sur chaque valuation. C'est une tautologie déguisée (celle de f <-> g).

let implique a b = Ou (Non a, b)

let f = implique (Var 0) (Var 1)                       (* x0 => x1 *)
let g = implique (Non (Var 1)) (Non (Var 0))           (* (non x1) => (non x0) *)
(* equivalentes f g  vaut  true *)

On construit les deux formules avec implique, puis equivalentes f g confirme par énumération qu'elles ont la même table de vérité : une implication équivaut toujours à sa contraposée. Représenter les connecteurs dérivés (=>, <->) par des combinaisons des trois de base est une technique récurrente.

let rec substitue f x g =
  match f with
  | Var i -> if i = x then g else Var i
  | Non h -> Non (substitue h x g)
  | Et (a, b) -> Et (substitue a x g, substitue b x g)
  | Ou (a, b) -> Ou (substitue a x g, substitue b x g)

Récursion sur la structure : on descend dans la formule et l'on remplace les feuilles Var x par g, en reconstruisant un nouvel arbre (les formules sont immuables). La substitution est l'opération de base de la réécriture de formules.

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).