You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 

52 lines
5.3 KiB

\section{Applications}
\subsection{Un petit langage de formules propositionnelles}
Puisque les diagrammes de décision binaires représentent des formules propositionnelles, il est naturel de vouloir créer un langage pour les formules propositionnelles. On se donne le type de syntaxe abstraite suivant:
\inputminted[bgcolor=darkBackground]{ocaml}{ml/expr_lang.ml}
On écrit un lexer et un parser, qui permettent d'écrire des formules ressemblant à cela: \texttt{(x0 || (x2 => x3) <=> x4 || !x1 => true || false}.
On suppose que le types de nos expression est dans un module \texttt{E} et que l'on dispose d'une fonction \texttt{int\_of\_var}. Alors, pour créer un diagramme de décision binaire à partir d'une expression, on procède ainsi:
\inputminted[bgcolor=darkBackground]{ocaml}{ml/expr_to_bdd.ml}
Le code complet contient toute une série de benchmarks permettant de comparer les $4$ implémentations différentes de nos diagrammes de décision binaires.
\subsection{Problème des N-reines}
\subsubsection{Présentation}
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$.
\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}
\subsubsection{Présentation du jeu}
Numberlink est un jeu de puzzle japonais, popularisé récemment par une version disponible sur téléphone. On a une grille avec des nombres dans certaines cases. Chaque nombre apparaît exactement deux fois. Il faut alors relier les paires de nombres identiques sans que les chemins ne se croisent et de telle sorte qu'il y ait au moins un chemin passant par chacune des cases.
\subsubsection{Représentation du problème}
Pour résoudre ce problème, on va le représenter sous une forme plus générale, utilisant des graphes non-orientés plutôt qu'une grille. On a aussi écrit un parser et un lexer qui permettent de passer d'une représentation textuelle d'une grille donnée à notre version sous forme de graphe.
\subsubsection{Difficulté}
Le problème dans le cas des graphes revient au problème du matching de chemins disjoints, qui est $NP$-complet. En effet, la version avec une seule paire de nombres à relier revient à trouver un chemin Hamiltonien entre deux sommets du graphe, ce qui est déjà un problème $NP$-complet.
\subsubsection{Réduction vers SAT}
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 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.
\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}.