7 lines
1.5 KiB
TeX
7 lines
1.5 KiB
TeX
\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.
|
|
|
|
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}.
|