Probleme – Quine sur les \textsc{fnc} : ce que la simplification fait gagner

1. La simplification, et c'est elle qui porte tout l'algorithme.

type litteral = string * bool          (* (nom, signe) : (p, false) est ¬p *)
type clause = litteral list            (* disjonction *)
type fnc = clause list                 (* conjonction *)

(* La FNC f où p vaut b. Deux effets, et ils sont différents :
   - une clause contenant le littéral SATISFAIT disparaît (elle est vraie) ;
   - dans les autres, le littéral contraire est RETIRÉ (il est faux).
   Précondition : aucune. Complexité : Theta(taille de f). *)
let simplifier f p b =
  f
  |> List.filter (fun c -> not (List.mem (p, b) c))
  |> List.map (List.filter (fun (q, _) -> q <> p))

La dissymétrie des deux lignes est le point délicat. La clause qui contient $p$ sous le bon signe est effacée — elle est vraie, elle ne contraint plus rien. La clause qui contient $p$ sous le mauvais signe maigrit — ce littéral-là ne peut plus la sauver. Confondre les deux, c'est écrire un algorithme qui rend « satisfiable » sur une formule qui ne l'est pas.

2. Quine.

(* Un modèle de f, ou None. Le modèle est partiel : les variables absentes
   du résultat peuvent prendre n'importe quelle valeur.
   Précondition : aucune. *)
let rec quine f =
  if f = [] then Some []                          (* plus de clause : VRAI *)
  else if List.exists (fun c -> c = []) f then None  (* clause vide : FAUX *)
  else
    let (p, _) = List.hd (List.hd f) in
    match quine (simplifier f p true) with
    | Some m -> Some ((p, true) :: m)
    | None ->
        match quine (simplifier f p false) with
        | Some m -> Some ((p, false) :: m)
        | None -> None

3. Terminaison et arrêts.

Variant : le nombre de variables distinctes de f. La deuxième ligne de simplifier retire toute occurrence de $p$ ; aucune variable n'est ajoutée. Le variant décroît donc strictement de $1$ à chaque appel récursif, et il est entier positif : la récursion a profondeur au plus $n$.

Les deux conditions d'arrêt sont duales, et il faut les tester dans cet ordre.

Ces deux conventions ne sont pas des choix arbitraires : ce sont les éléments neutres. Une conjonction sans facteur vaut $\top$, une disjonction sans terme vaut $\perp$ — exactement comme une somme vide vaut $0$ et un produit vide vaut $1$.

Correction : par récurrence sur le variant. Si $f$ est vide, toute valuation convient. Si une clause est vide, aucune ne convient. Sinon, $f$ est satisfiable si et seulement si $f[p:=V]$ l'est ou $f[p:=F]$ l'est — car toute valuation donne à $p$ l'une des deux valeurs —, et simplifier f p b est bien $f[p:=b]$ d'après la spécification ci-dessus.

Complexité : $O(2^n)$ appels dans le pire cas, chacun en $\Theta (|f|)$ ; mais la clause vide interrompt une branche avant sa profondeur maximale, et c'est ce qui fait toute la différence en pratique.

4. Les mesures.

La dernière ligne est la plus parlante : la même formule, traitée par le quine sans simplification de l'exercice 20.5, demande $32767$ appels — soit l'arbre binaire complet. Avec simplification : trois. Le facteur $10000$ ne tient qu'à ceci : dès que $p$ est fixée, la clause $(p)$ ou la clause $(\neg p)$ devient vide, et les $2^{13}$ valuations des autres variables ne sont jamais visitées.