> 6.   Rappelez la définition inductive de la **taille** d'une formule propositionnelle. Donnez les tailles des formules `ex1, ex2, ex3`.
> 7.   Déduisez-en une fonction récursive `taille : formule -> int`.
> 8.   Rappelez la définition inductive de la **hauteur** d'une formule propositionnelle. Donnez les hauteurs des formules `ex1, ex2, ex3`.
> 9.   Déduisez-en une fonction `hauteur : formule -> int`.
> 10.   Calculez soigneusement les complexités temporelles des fonctions `taille` et `hauteur`.
> 11.   Rappelez la définition inductive de $`varphi[psi/x], text{ avec } varphi, psiin mathcal P_mathcal V, xin mathcal V`$ (**substitution**). Déduisez-en une fonction `substitue : formule -> int -> formule -> formule`.
> 12.   Rappelez la définition inductive de l’ensemble des **sous-formules** d’une formule propositionnelle. Déduisez-en une fonction `ensemble_sous_formules : formule -> formule list`. La liste renvoyée pourra éventuellement contenir des doublons (dans le cas où la formule en paramètre contient plusieurs fois la même sous-formule).



## II. Sémantique des formules propositionnelles

On utilise dans cette partie le même type `formule` défini dans la partie précédente.

### 1. Évaluation d'une formule

On définit une **valuation** comme un tableau de booléens :

```ocaml
type valuation = bool array
```

Si `v` est de type `valuation`, alors `v.(i)` donne la valeur de vérité associée à la variable propositionnelle `Var i`.

Voici par exemple la liste des 8 valuations existantes pour la formule correspondant à la variable `ex1` définie dans la partie précédente :

```ocaml
let vals_3 = [ [|false;false;false|]; [|true;false;false|]; [|false;true;false|]; [|true;true;false|]; [|false;false;true|]; [|true;false;true|]; [|false;true;true|]; [|true;true;true|] ]
```

>   1.   Rappelez la définition inductive de $`[![varphi]!]_text v,text{ avec } varphiin mathcal P_mathcal V`$ et `v` une valuation (**évaluation**). Déduisez-en une fonction `evaluation : formule -> valuation -> bool`.
>   3.   Déterminez à la main si la valuation `[|true;false;true|]` est un **modèle** de la formule correspondant à la variable `ex1`, puis vérifiez votre réponse avec la fonction `evaluation`.
>   4.   Écrivez une fonction `modeles : formule -> valuation list -> valuation list` telle que `modeles phi valuations` renvoie $`text{Mod}(varphi)`$, avec le paramètre `valuations` étant la liste de toutes les valuations existantes pour la formule.
>   5.   Dressez à la main la table de vérité de la formule correspondant à la variable `ex1` afin de déterminer ses modèles, puis vérifiez votre réponse avec la fonction `modeles` et les valuations `vals_3`.
>   6.   Quelle est la complexité de la fonction `evaluation` ? Combien une formule possède-t-elle de valuations existantes ? Quelle est donc la complexité de la fonction `modeles` ?
>   7.   À partir de la fonction `modeles`, comment pourrait-on déterminer si une formule est **satisfiable** ? **tautologique** ? **antilogique** ?

### 2. Conséquence et équivalence sémantique

On rappelle que :

*   $`psiinmathcal P_mathcal V text{ est une conséquence sémantique de }varphiinmathcal P_mathcal V, text{ noté } varphivDashpsi, text{ ssi }Mod(varphi)subset Mod(psi)`$
*   $`psiinmathcal P_mathcal V text{ est équivalente sémantiquement à }varphiinmathcal P_mathcal V, text{ noté } varphiequivpsi, text{ ssi }Mod(varphi)= Mod(psi)`$

>   7. Écrivez une fonction `consequence : formule -> formule -> valuation list -> bool` telle que `consequence phi psi valuations` détermine si $`varphivDash psi`$ avec `valuations` la liste de toutes les valuations existantes. Exemples :
>
>       ```ocaml
>       # let vals_4 = [[|false;false;false;false|]; [|true;false;false;false|]; [|false;true;false;false|]; [|true;true;false;false|]; [|false;false;true;false|]; [|true;false;true;false|]; [|false;true;true;false|]; [|true;true;true;false|]; [|false;false;false;true|]; [|true;false;false;true|]; [|false;true;false;true|]; [|true;true;false;true|]; [|false;false;true;true|]; [|true;false;true;true|]; [|false;true;true;true|]; [|true;true;true;true|]] ;;
>       # consequence ex1 ex2 vals_4 ;;
>       - : bool = false
>       # consequence ex1 (Ou (Var 2, Ou (Non (Var 0), Et (Non (Var 1), Non (Var 2))))) vals_4 ;;
>       - : bool = true
>       ```
>
>   2. Écrivez aussi une fonction `equivalence : formule -> formule -> valuation list -> bool`. Exemples :
>
>       ```ocaml
>       (* vals_4 vient de l'exemple précédent *)
>       # equivalence ex1 ex2 vals_4 ;;
>       - : bool = false
>       # equivalence ex1 (Ou (Non (Var 0), Et (Non (Var 1), Non (Var 2)))) vals_4 ;;
>       - : bool = true
>       ```

Pour étudier la satisfiabilité d'une formule, quelques équivalences sémantiques permettent de simplifier la formule pour en éliminer les constantes logiques :

![](img/logique/regles_quine.png)

> 9. Écrivez une fonction `elimine_constantes : formule -> formule` qui prend en entrée une formule $varphi$ et utilise les règles ci-dessus afin de renvoyer une formule $`varphi'`$ telle que $`varphi'equiv varphi`$, et soit $varphi'$ est réduite à une constante, soit elle ne contient aucune constante. Exemples :
>

>     ```ocaml
>     # elimine_constantes ex2 ;;
>     - : formule = Non (Var 3)
>     # elimine_constantes ex3 ;;
>     - : formule = Bottom
>
> 12. Montrez par induction structurelle sur `phi` que si `phi` ne contient pas de variable alors `elimine_constantes phi` est réduite à une constante.

### 3. Algorithme de Quine

Le « **problème SAT** » consiste à déterminer si une formule propositionnelle est satisfiable.

>   11.   De quel type de problème s'agit-il ?

La première manière de résoudre le problème SAT est une approche par *force brute* : tester toutes les valuations possibles. C'est ce que fait la fonction `modeles` écrite plus haut, et ce n'est pas très efficace. La seconde manière de résoudre le problème SAT est l'**algorithme de Quine**, qui utilise une approche par *backtracking*.

L'algorithme de Quine consiste, à partir d'une formule `f`, à :

* Calculer `f' = elimine_constantes f`.
* S'il reste au moins une variable propositionnelle dans `f’` :
    * sélectionner arbitrairement une variable $x$ restante dans `f’` ;
    * tester récursivement si $`texttt{f'}[top/x]`$ est satisfiable ;
    * tester récursivement si $`texttt{f'}[bot/x]`$ est satisfiable.
* Sinon, conclure.

Comme tout algorithme de backtracking, on peut dessiner l'arbre correspondant à l'algorithme de Quine.

Considérons par exemple la formule $`varphi = (alor b)land (lnot b lor lnot c)land(lnot a lor c)land(alor c)`$, qui est donc la racine de notre arbre.

*   On sélectionne la variable `a` arbitrairement, on va la substituer par $`bot`$ puis poursuivre (sous-arbre gauche) et la substituer par $`top`$ puis poursuivre également (sous-arbre droit).

    Étudions par exemple la branche droite. Par substitution on obtient la formule $`varphi' = (toplor b)land (lnot b lor lnot c)land(lnot top lor c)land(toplor c)`$, puis en appliquant les règles de simplification pour enlever les constantes on trouve donc $`varphi' equiv topland (lnot b lor lnot c)land(bot lor c)landtop equiv (lnot b lor lnot c)land c`$.

*   On sélectionne à partir de là arbitrairement une variable restante, disons `b`. On substitue `b` par  $`bot`$ puis on poursuit (sous-arbre gauche) et on la substitue par $`top`$ puis on poursuit également (sous-arbre droit).

    Suivons cette fois la branche gauche. Par substitution puis simplification on obtient $`varphi'' = (lnot bot lor lnot c)land c equiv (top lor lnot c)land c equiv top land c equiv c`$.

*   On sélectionne la dernière variable restante, `c`, qu'on substitue à nouveau par les deux constantes logiques.

*   Il ne reste plus aucune variable, les feuilles sont étiquetées par des constantes.

Voici l'arbre correspondant au cheminement qu'on vient de faire :

![](img/logique/quine.png)

> 12.   Complétez les branches de l'arbre non détaillées ci-dessus.
> 16.   À quelle condition sur l'arbre obtenu la formule est-elle satisfiable ? une tautologie ? une antilogie ? La formule de l’exemple ci-dessus est-elle donc satisfiable ? une tautologie ? une antilogie ?

À chaque étape de l'algorithme de Quine, on sélectionne la prochaine variable à substituer arbitrairement. On choisira ici de prendre la plus grande variable restante.

>   14.   Écrivez une fonction `max_var : formule -> int option` qui calcule le numéro maximal d’une variable propositionnelle utilisée dans une formule. Le type `option` sert au cas où la formule ne contient aucune variable. La complexité devra être linéaire en la taille de la formule. Exemples :
>
>        ```ocaml
>        # max_var ex1 ;;
>        - : int option = Some 2
>        # max_var ex2 ;;
>        - : int option = Some 3
>        # max_var ex3 ;;
>        - : int option = None
>        ```

On utilisera le type suivant pour représenter l’arbre de Quine :

```ocaml
type arbre_quine =
	| Feuille_top
	| Feuille_bottom
	| Noeud_interne of int * arbre_quine * arbre_quine
```

Pour tester vos codes, voici la formule de l’exemple précédent :

```ocaml
(* ((a ∨ b) ∧ (¬b ∨ ¬c)) ∧ ((¬a ∨ c) ∧ (a ∨ c))
   avec c = Var 0, b = Var 1, a = Var 2 *)
let (exemple : formule) =   Et  (   Et  (   Ou (Var 2, Var 1),
                                            Ou (Non (Var 1), Non (Var 0))
                                        ),
                                    Et  (   Ou (Non (Var 2), Var 0),
                                            Ou (Var 2, Var 0)
                                        )
                                )
```

>   15.   Écrivez une fonction `quine : formule -> arbre_quine` qui prend en paramètre une formule et renvoie l'arbre associé par l'algorithme de Quine.
>   18.   Écrivez une fonction `satisfiable_quine : arbre_quine -> bool` qui détermine si une formule est satisfiable depuis l'arbre de l'algorithme de Quine de cette formule.
>   19.   Si la formule est satisfiable, comment retrouver un modèle depuis l’arbre de Quine ?

Le problème SAT est un problème absolument central en informatique, parce que d’innombrables problèmes de décision se réduisent naturellement à lui. **Il faut savoir implémenter l'algorithme de Quine.** 

>   18.   Avec l'algorithme de Quine, écrivez une fonction `tautologie : formule -> bool` qui détermine si une formule propositionnelle est une tautologie. Cette fonction ne doit pas passer par le type `arbre_quine`.



## III. Exercices

>   **Exercice 1 : Fonctions supplémentaires sur les formules propositionnelles**
>
>   *Syntaxe*
>
>   1. Écrivez une fonction `nb_var_distinctes : formule -> int` qui renvoie le nombre de variables propositionnelles distinctes apparaissant dans une formule. *On essaiera d'être efficace.* Exemples :
>
>       ```ocaml
>       # nb_var_distinctes ex1 ;;
>       - : int = 3
>       # nb_var_distinctes ex2 ;;
>       - : int = 2
>       # nb_var_distinctes ex3 ;;
>       - : int = 0
>       ```
>
>   2. Écrivez une fonction `sous_formule : formule -> formule -> bool` qui détermine si une formule est une sous-formule d'une autre.
>
>   *Équivalence sémantique*
>
>   Soit $`x in mathcal V, varphiinmathcal P_mathcal V`$. On peut définir le quantificateur universel ainsi : $`forall x. varphi equiv varphi[top/x]land varphi[bot/x]`$
>
>   3.   Déduisez-en une fonction `quantificateur_universel : int -> formule -> formule` telle que `quantificateur_universel x phi` renvoie une formule sémantiquement équivalente à $`forall x. varphi`$.
>   4.   En vous inspirant de l'équivalence précédente, donnez une définition possible du quantificateur existentiel, et déduisez-en une fonction `quantificateur_existentiel : int -> formule -> formule`.
>
>   On peut utiliser la fonction `equivalence` écrite plus haut pour vérifier la validité de certaines équivalences sémantiques fondamentales. Par exemple la double négation $`varphiequivlnotlnotvarphi`$ peut être vérifiée ainsi :
>
>   ```ocaml
>   equivalence (Var 0) (Non (Non (Var 0))) [[|false|]; [|true|]]
>   ```
>
>   5.   Montrez les lois de De Morgan à l'aide de la fonction `equivalence`.
>
>   *Algorithme de Quine*
>
>   6.   Avec l'algorithme de Quine, écrivez une fonction `valuation_quine : formule -> valuation option` qui renvoie une valuation qui satisfait la formule propositionnelle. Le type `option` sert à gérer le cas où la formule n'est pas satisfiable.
>   7.   Avec l'algorithme de Quine, écrivez une fonction `antilogie : formule -> bool` qui détermine si une formule propositionnelle est une antilogie.
>   8.   Montrez que l'algorithme de Quine termine.

>   **Exercice 2 : portée des variables**
>
>   Les variables propositionnelles seront dans cet exercice de type `'a`.
>
>   1.   Modifiez le type `formule` afin d'y ajouter les deux quantificateurs ainsi que les connecteurs d'implication et d'équivalence. On appelle ce type `'a formule_complete`.
>

>   2.   Définissez dans une variable `ex_complet : char formule_complete` la formule propositionnelle correspondant à l'arbre suivant :
>
>        ![](img/logique/arbre.png)
>
>   Une occurrence d'une variable $x$ dans une formule est un nœud de l'arbre étiqueté par $x$.
>
>   Une occurrence de $x$ est dite *libre* si le chemin reliant l'occurrence à la racine ne contient pas de nœud $`forall x`$ (ou plus précisément, de nœud $`forall`$ dont le fils gauche est $x$) ni de nœud $`exists x`$. Une occurrence de $x$ est dite *liée* dans le cas contraire.
>
>   Une variable est dite libre dans une formule si elle a au moins une occurrence libre, liée si elle a au moins une occurrence liée.
>
>   3.   Écrivez une fonction `est_liee : 'a formule_complete -> 'a -> bool` qui indique si une variable est liée dans une formule.
>   4.   Écrivez une fonction `est_libre : 'a formule_complete -> 'a -> bool` qui indique si une variable est libre dans une formule.
>
>   La *portée* d’une variable liée $x$ est la sous-formule $`varphi`$ des formules $`forall x. varphi text{ et }exists x. varphi`$.
>
>   5.   Écrivez une fonction `portee : 'a formule_complete -> bool * 'a -> 'a formule_complete option` qui prend en paramètre une formule et un couple `(b, i)` où `b` vaut `true` pour désigner le quantificateur universel et `false` pour désigner le quantificateur existentiel, et `i` désigne une variable propositionnelle ; et renvoie sa portée. S'il y a plusieurs occurrences liées de cette variable, on renverra la sous-formule située la plus à gauche dans l'arbre de la formule. Si elle n'apparaît pas dans la formule, on renverra `None`.

>   **Exercice 3 : résolution par force brute du problème SAT**
>
>   On reprend dans cet exercice les types `formule` et `valuation` définis dans les premières parties du TP.
>
>   L’algorithme de Quine est une approche par backtracking de la résolution de problème SAT. Comme tout problème de décision, on peut aussi le résoudre avec une approche par force brute.
>
>   Cette approche suit en fait un principe similaire à celui des tables de vérité : on évalue la formule propositionnelle pour chaque valuation existante et on regarde si l’une d’elle donne la valeur de vérité V.
>
>   On propose de construire l’ensemble des valuations existantes ainsi :
>
>   *   On commence par la valuation associant la valeur de vérité F à toutes les variables.
>   *   Pour passer à la valuation suivante :
>       *   On cherche la plus grande variable propositionnelle qui a pour valeur de vérité F.
>       *   On passe sa valeur de vérité à V.
>       *   On passe la valeur de vérité de toutes les variables propositionnelles plus grandes à F.
>
>   1.   En appliquant cette méthode pour passer d’une valuation à la suivante, quelle sera la seconde valuation testée ? la troisième ? quatrième ? dernière ?
>
>   On définit l’exception suivante :
>
>   ```ocaml
>   exception Derniere_valuation
>   ```
>
>   2.   Écrivez une fonction `valuation_suivante : valuation -> unit` qui modifie la valuation passée en paramètre pour construire la valuation suivante selon la méthode décrite ci-dessus. Cette fonction lève l’exception `Derniere_valuation` si la valuation passée en paramètre était la dernière à tester.
>   3.   Écrivez une fonction `satisfiable_brute : formule -> bool` qui détermine si une formule est satisfiable en essayant toutes les valuations possibles (jusqu'à les épuiser ou en trouver une convenable).
>   4.   Écrivez de même deux fonctions `tautologie_brute : formule -> bool` et `antilogie_brute : formule -> bool` qui déterminent respectivement si une formule propositionnelle est une tautologie ou antilogie avec une approche par force brute.



## Pour aller plus loin

> 1. Modifiez la fonction `ensemble_sous_formules` de la première partie pour que la liste renvoyée ne contienne aucun doublon.
> 2. Reprenez les fonctions du TP avec l'implémentation en C des formules propositionnelles.


---

Par *Justine BENOUWT*