Réduction de Diagramme de Décision Binaire

Une technique basée sur des graphes pour représenter des fonctions booléennes comme des graphes acycliques orientés (diagrammes de décision binaires, BDD) avec des règles de réduction (fusion des sous-graphes isomorphes et élimination des tests redondants) qui peuvent produire une forme canonique réduite et ordonnée (ROBDD) pour un ordre de variables fixé, permettant des vérifications d'équivalenc