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.
 
 
 
 
 

6 lines
1.5 KiB

\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}.