more

src/app.tex

@@ -20,7 +20,9 @@
 
     Le problème des N-reines est le suivant. Supposons que l'on dispose d'une grille de taille $N \times N$. On veut disposer une reine sur chaque ligne, soit un total de $N$ reines et ce, de telle sorte que chacune des reines soit à l'abri des autres selon les règles employées aux échecs. C'est-à-dire, pour une reine $r$ donnée : il n'y a aucune autre reine sur la même ligne, aucune autre reine sur la même colonne et aucune autre reine sur l'une des diagonales passant par la case où se trouve $r$.
 
-    TODO
+    \subsubsection{Implémentation et résultats}
+      On va chercher ici à calculer l'ensemble des solutions possibles pour un $N$ donné et les compter. L'implémentation consiste à exprimer les contraintes présentées précédemment directement en un diagramme de décision binaire et est relativement simple.
+      Lorsque l'on demande le résultat pour $N = 8$, on obtient bien $92$ solutions et ce, instantanément\footnote{Aucun benchmark précis n'a été réalisé.}. Lorsque l'on passe à $N = 9$, on obtient $352$ en environ deux secondes et enfin, à partir de $N=10$ on obtient $724$ mais le temps de calcul dépasse les dix secondes.
 
   \subsection{Numberlink}
 
@@ -38,12 +40,13 @@
 
     \subsubsection{Réduction vers SAT}
 
-    En reprenant l'approche dans TODO, on a réduit le problème vers SAT, et ce, en utilisant notre petit langage d'expressions propositionnelles présenté précedemment.
+    En reprenant l'approche donnée par \href{https://www.lix.polytechnique.fr/~pilaud/}{\bsc{Vicent Pilaud}} dans \href{https://www.lix.polytechnique.fr/~pilaud/enseignement/TP/DIX/INF421/1819/}{un projet de programmation} de l'École polytechnique, on a réduit le problème vers SAT, et ce, en utilisant notre petit langage d'expressions propositionnelles présenté précedemment. En effet, contrairement au sujet de programmation évoqué ci-dessus, on utilisera non pas un SAT-solver, mais notre implémentation des diagrammes de décision binaire.
 
-    Il s'agit de générer les formules correspondant aux contraintes présentées dans TODO, ce qui n'est pas complètement trivial, mais s'écrit de façon assez agréable lorsque l'on s'y prend correctement. Par exemple, la contrainte qui nous dit que pour tout chemin $i$, l'ensemble des sommets consécutifs sur le chemin $i$ sont adjacents dans notre graphe, s'écrit ainsi:
+    Il s'agit de générer les formules correspondant aux contraintes présentées dans le sujet, ce qui n'est pas complètement trivial, mais s'écrit de façon assez agréable lorsque l'on s'y prend correctement. Par exemple, la contrainte qui nous dit que pour tout chemin $i$, l'ensemble des sommets consécutifs sur le chemin $i$ sont adjacents dans notre graphe, s'écrit ainsi:
 
     \inputminted[bgcolor=darkBackground]{ocaml}{ml/numlink_cond.ml}
 
     Après avoir encodé l'ensemble de notre problème ainsi, on peut utiliser la fonction de translation vers les diagrammes de décision binaires pour construire le diagramme correspondant à une instance donnée. On pourra alors ensuite voir immédiatement s'il existe une solution par exemple, ou bien, demander une solution au hasard. On pourra aussi vérifier qu'une solution donnée en est bien une.
 
-    TODO
+    \subsubsection{Résultats}
+      Malheureusement, on arrive rapidement à des formules propositionnelles dont la taille est trop importante. La construction de nos diagrammes de décision binaires est alors bien trop lente pour être utilisée. En effet, contrairement à un SAT-solver, le diagramme de décision binaire construit toutes les solutions possibles. Une solution serait de modifier l'encodage vers SAT, en utilisant par exemple une autre représentation du problème, comme cela est d'ailleurs suggéré dans le sujet de \bsc{Vincent Pilaud}.

src/bdd.tex

@@ -1,4 +1,4 @@
-\section{Les diagrammes de décision binaire}
+\section{Les diagrammes de décision binaires}
   \subsection{La logique propositionnelle}
     \subsubsection{Les propositions}
       \paragraph{}
@@ -57,6 +57,7 @@
         \end{center}
         En fait, on a en quelque sorte développé la fonction, elle est \enquote{partiellement calculée}. Dans le cas d'une tautologie ou d'une contradiction, on aurait même complètement calculé la valeur de la proposition.
   \subsection{Représentation formelle}
+  On utilise ici l'approche présentée dans \cite{Andersen97}.
     \subsubsection{Opérateur \texttt{if-then-else}}
       On définit l'opérateur \texttt{if-then-else}, de $\mathbb{B}^3$ vers $\mathbb{B}$, et noté $P \rightarrow Q_1, Q_2$ ainsi:
 
@@ -64,7 +65,7 @@
 
       Ce qui se lit: \enquote{Si $P$, alors, $Q_1$, sinon, $Q_2$.}.
     \subsubsection{Forme normale \texttt{if-then-else}}
-      On dit qu'une formule propositionnelle est en forme normale \texttt{if-then-else} (FNI) si elle est construite uniquement à partir de l'opérateur \texttt{if-then-else} et des constantes $\top$ et $\bot$ ; et de telle sorte que le premier opérande de l'opérateur \texttt{if-then-else} est toujours une variable.
+    On dit qu'une formule propositionnelle est en forme normale \texttt{if-then-else} (FNI) si elle est construite uniquement à partir de l'opérateur \texttt{if-then-else} et des constantes $\top$ et $\bot$ ; et de telle sorte que le premier opérande de l'opérateur \texttt{if-then-else} est toujours une variable. On recommande la lecture de \cite{} au lecture curieux d'en apprendre plus à ce sujet.
     \subsubsection{Expansion de \bsc{Shannon}}
       On note $P[Q_1/Q_2]$  la proposition $P$ dans laquelle on a substitué toutes les occurences de $Q_1$ par $Q_2$. On a alors:
         \[P = Q \rightarrow P[Q/\top], P[Q/\bot]\]
@@ -80,6 +81,7 @@
           \[= P \rightarrow (Q \rightarrow \top, \bot), (Q \rightarrow \bot, \bot) \]
 
     \subsubsection{Passage en graphe orienté acyclique}
+    À partir de maintenant, on ne poursuit non plus sur l'approche de \cite{Andersen97}, mais sur celle de \cite{Bryant86}.
       \paragraph{}
         Une proposition sous FNI peut être représentée comme un arbre binaire, sur notre exemple précédent, cela donnerait le résultat suivant:
           \begin{center}

src/conclusion.tex

@@ -1 +1,4 @@
 \section{Conclusion}
+  De la représentation des entiers dans le modèle d'exécution d'OCaml à la bonne façon de définir un type partiellement opaque pour permettre la fonctorisation, ces travaux de recherche ont été l'occasion d'étudier de très nombreux aspects du langage OCaml. Cela dans le but de modéliser un formalisme mathématique: la logique propositionnelle. Ces aller-retours permanents entre théorie et pratique ont été une chance, ils m'ont en effet permis d'apprendre énormément sur le sujet des diagrammes de décision binaires et diverses techniques telles que le hashconsing, la mémoïsation, ou même des structures de données telles que les éphémérons.
+
+  Je tiens particulièrement à remercier Jean-Christophe pour son encadrement. Les mercredi après-midis passés en sa compagnie ont été des plus enrichissants ! Il m'a dit aimer enseigner et je dois bien avouer que cela se ressent dans sa façon d'expliquer les choses. De plus, il est intarissable sur une infinité de sujets passionnants, ce qui mène souvent à de nombreuses disgressions\footnote{Pourquoi en 2006 fallait-il utiliser un nombre premier pour initialiser la taille d'une table de hachage alors qu'aujourd'hui il est préférable d'utiliser une puissance de deux ? Pour le savoir, demandez à Jean-Christophe !}, il faut alors employer la technique du \emph{backtracking}\footnote{Serait-ce là l'origine de son pseudonyme sur GitHub ?} pour reprendre le fil, mais c'est toujours un plaisir. Alors Jean-Christophe, merci !

src/implem.tex

@@ -14,7 +14,7 @@
 
       \inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_order.ml}
 
-    Pour comparer deux diagrammes de décisions binaire, on se contentera ensuite de récupérer leur image par \texttt{get\_order} et d'utiliser la comparaison sur les entiers d'OCaml.
+    Pour comparer deux diagrammes de décision binaire, on se contentera ensuite de récupérer leur image par \texttt{get\_order} et d'utiliser la comparaison sur les entiers d'OCaml.
     \subsubsection{Smart constructor, fonctions auxiliaires et constantes}
     On introduit ensuite un \emph{smart constructor} permettant de créer un nouveau sommet:
 
@@ -155,7 +155,8 @@
   Le point intéressant est que la mémoïsation se fait elle aussi en temps constant: on utilise l'égalité physique pour comparer deux valeurs et on se contente de récupérer le champ \texttt{tag} pour hacher une valeur.
 
   \subsection{Fonctorisation des implémentations précédentes}
-  %%%%% FONCTORISATION DE LA FONCTORISATION
+
+  Cette section mais surtout, le code associé, fait un usage intensif des foncteurs d'OCaml et de son système de modules. Le lecteur qui n'est pas familier avec ce système peut se reporter vers \cite{Leroy00} qui en fait une présentation détaillée. Il est important de noter que ce système de module est extrêmement puissant et permet beaucoup de choses. Il est d'ailleurs, en théorie, adaptable à n'importe quel langage pour lequel on dispose d'un \emph{typechecker}.
 
   Afin de pouvoir mesurer l'impact sur l'usage mémoire et le temps de calcul du hashconsing et de la mémoïsation, on a créé un foncteur \texttt{Bdd.Make} paramétré par un module contenant un module de hashconsing et un module de mémoïsation.
 
@@ -200,3 +201,6 @@
 
   \subsubsection{\texttt{count\_sat}}
   Le cas de \texttt{count\_sat} est un peu plus compliqué car l'utilisateur doit saisir le nombre de variables existantes. On utilise alors le fait que les variables sont ordonnées pour calculer à chaque fois le nombre de variables qui n'apparaissent pas dans la formule, et on multiplie correctement le nombre possible de solutions en faisant un peu d'arithmétique. On a ici aussi dû utiliser de la mémoïsation: en effet un sous-diagramme peut apparaître plusieurs fois dans notre parcours.
+
+   \subsection{Outils utilisés}
+    En plus du langage OCaml, plusieurs outils ont été utilisés pour notre implémentation: le \emph{build system} \href{https://dune.build}{Dune}, le générateur de parser \href{https://gallium.inria.fr/~fpottier/menhir/}{Menhir}, le framework de test \href{https://github.com/mirage/alcotest}{alcotest}, \href{https://github.com/aantron/bisect_ppx}{bisect\_ppx} pour la couverture du code et enfin, \href{https://github.com/LexiFi/landmarks}{landmarks} pour le profilage du code. Merci à leurs auteurs.

src/introduction.tex

@@ -1,4 +1,6 @@
 \section{Introduction}
+  La logique propositionnelle est un formalisme largement utilisé en mathématiques et en informatique. Il n'existe probablement pas un seul programme informatique qui ne contienne des injonctions telles que \emph{Si A, alors, faire B}. De même, en informatique théorique, le problème de satisfiabilité des formules propositionnelles est l'exemple typique donné de problème NP-complet. C'est en effet un problème difficile et énormément de travaux de recherches lui étant rattaché on été menés. Par exemple, au travers des SAT-solvers.
 
-TODO \cite{Leroy00} \cite{Knuth11} \cite{Andersen97} \cite{Bryant86}
-TODO: lien vers le repo
+Les diagrammes de décision binaires sont une autre approche, moins répandue, quant à la façon de représenter les formules de la logique propositionnelle. Il est tout de même intéressant de noter que \bsc{Donal Knuth} a dit a propos des diagrammes de décision binaires qu'ils sont \enquote{one of the only really fundamental data structures that came out in the last twenty-five years.}. Profitons d'ailleurs de l'occasion pour mentionner \cite{Knuth11} dont la lecture a beaucoup aidé pour la compréhension des diagrammes de décision binaires.
+
+On va ici introduire les diagrammes de décision binaires et leur lien avec la logique propositionnelle formellement. Puis, on présentera l'implémentation qui en a été réalisée. Pour finir, quelques applications seront détaillées. Le code de l'implémentation est disponible sur un \href{https://git.zapashcanon.fr/zapashcanon/bdd}{dépôt git}.

src/main.tex

@@ -18,9 +18,9 @@
 \input{app.tex}
 \input{conclusion.tex}
 
-\appendix
+%\appendix
 
-\input{appendix.tex}
+%\input{appendix.tex}
 
 \printbibliography{}