Probleme – Un évaluateur, un compteur de modèles, un testeur de tautologie

1. Les modèles.

(* Toutes les valuations sur vs. Il y en a 2^|vs|.
   Précondition : vs sans doublon. *)
let rec valuations = function
  | [] -> [[]]
  | p :: reste ->
      List.concat_map (fun l -> [(p, true) :: l; (p, false) :: l])
                      (valuations reste)

(* La valeur que la liste d'association l donne à p ; false par défaut,
   ce qui ne sert jamais si l porte toutes les variables de la formule. *)
let lire l p = try List.assoc p l with Not_found -> false

(* Liste des modèles de f, comme listes d'association sur variables f.
   Précondition : aucune. Postcondition : le résultat contient exactement
   les valuations v de variables f telles que [[f]]_v = V. *)
let modeles f =
  List.filter (fun l -> evalue (lire l) f) (valuations (variables f))

2. Les trois prédicats.

let nb_variables f = List.length (variables f)
let satisfiable f = modeles f <> []
let tautologie f =
  List.for_all (fun l -> evalue (lire l) f) (valuations (variables f))
let antilogie f = not (satisfiable f)

Un seul parcours suffit, et il ne faut surtout pas le faire trois fois. Chacun des trois prédicats est un quantificateur sur la même table : $\exists$ pour la satisfiabilité, $\forall$ pour la tautologie, et l'antilogie est la négation du premier. Écrits comme ci-dessus, satisfiable et tautologie s'arrêtent dès qu'ils savent — List.for_all rend false au premier contre-modèle. C'est le même bénéfice que la paresse du chapitre chap:langage-c, et c'est ce que perd la version qui construit d'abord toute la liste.

3. La grille complète pour modeles.

Spécification. Entrée : une formule $f$. Sortie : la liste des valuations sur $\mathrm{Var}(f)$ qui satisfont $f$, chacune donnée comme liste d'association. Aucune précondition.

Terminaison. valuations récurre sur une liste strictement plus courte : variant $=$ la longueur de la liste. evalue récurre sur un sous-arbre strict : induction structurelle. List.filter parcourt une liste finie. Tout termine.

Correction. Par récurrence sur $\mathtt{vs}$ : valuations [] rend [[]], l'unique valuation vide ; et si valuations reste énumère les $2^k$ valuations sur reste sans répétition, alors préfixer chacune par $(p,V)$ puis par $(p,F)$ en donne $2^{k+1}$, deux à deux distinctes, et toutes. La correction de evalue est celle du cours (induction structurelle, la fonction reproduit la définition). Le filtre garde donc exactement les modèles.

Complexité. $|\mathtt{valuations}|=2^n$ listes de longueur $n$, construites en $\Theta (n{2}^n)$. Chaque évaluation coûte $O(|f|)$ nœuds, chacun consultant List.assoc en $O(n)$. Total : $\Theta (2^n\cdot n\cdot |f|)$ en temps, et $\Theta (n{2}^n)$ en espace — c'est là que le bât blesse, car on matérialise la table.

4. Le piège du comptage. L'écriture List.length (modeles f) = 1 lsl n est fausse pour deux raisons distinctes, et il faut les nommer toutes les deux.

D'abord, elle est coûteuse pour rien : elle calcule tous les modèles avant de conclure, là où un seul contre-modèle suffirait. Sur une formule qui échoue à la première ligne, on paie $2^n$ au lieu de $1$.

Ensuite, et c'est plus grave, n y désigne quoi ? Si c'est nb_variables f, le test est correct mais fragile ; si c'est un nombre de variables fixé par le contexte — celui d'un ensemble de formules, par exemple —, le test devient faux : $p\vee \neg p$ a $2$ modèles sur ses propres variables et $8$ sur $\{p,q,r\}$, et elle est tautologique dans les deux cas. Le nombre de modèles n'a de sens que relativement à un ensemble de variables déclaré. La formulation par $\forall$ n'a pas ce défaut : elle ne mentionne aucun nombre.