, b(n ), op); h(n ) := A(h(n), h(n ), op); (n ) : let n = new (v(n)) in b(n ) := A(b(n), n , op); h(n ) := A(h(n), n , op); (n) : let n = new (v(n )) in b(n ) := A(n, b(n ), op); h(n ) := A(n, h(n ), op), analyse de cas (1) v(n) = v(n ) ? V : let n = new (v(n)) in b(n ) := A(b(n)
, Exercice 77 Montrez que l'application d'une opération de restriction sur un BDD réduit peut ne pas produire un BDD réduit
, 2 ? 2 une opération binaire. On remarque que l'opération commute avec l'expansion de Shannon (6.1), ` a savoir : A op B ? x, Application Soient A et B deux formules avec var (A) ? var (B) ? {x 1
, 1, on définit un algorithme A (A pour application) qui construit un BDD A(?, ? ) définissant la fonction : f ? (x 1, On applique cette remarque aux BDD. Soient ?, ? deux BDD qui définissent les fonctions f ? : 2 n ? 2 et f ? : 2 n ? 2 par rapport aux variables x 1 <
, Dans la description de l'algorithme on suppose que new (x) est une fonction qui retourne un nouveau noeud n avec v(n) = x, que le champs b(n) et h(n) d'un noeud n sont modifiables (la notation ' :=' indique une modification du contenu de ces champs) et que n b pour b ? 2 sont deux noeuds prédéfinis tels que v(n b ) = b. Dans le cas (1), les deux noeuds ont la même variable commé etiquette, L'algorithme visite les BDD ? et ? en profondeur d'abord. En supposant que n et n soient les racines de ? et ? , l'appel A(n, n , op) retourne la racine d'un BDD qui définit la fonction (6.3)
, Unedeuxì eme optimisation est d'arrêter les appels récursifs chaque fois qu'on arrivè a une feuille d'un des sous-diagrammes avec la propriété que la valeur de la feuille est suffisante pour déterminer le résultat de l'opération op. Enfin, il est possible Diagrammes de décision binaire de modifier l'algorithme de façonfaçonà ce qu'il recherchè a la volée une des simplifications possibles ; de cette façon, on peut générer directement un BDD réduitréduità partir de BDD réduits, Remarque 13 Cet algorithme peutêtrepeutêtre amenéamené`amenéàamenéàévaluer plusieurs fois le même couple de sous-diagrammes. PouréviterPouréviter cela, on peut utiliser une optimisation standard en programmation dynamique qui consistè a garder dans une table de hachage les couples de sousdiagrammes déjà visités
, Exercice 78 Utilisez l'algorithme A pour construire un BDD réduit qui définit la fonction : AND(NOR(x, y), AND(z, w))
, Exercice 79 Un additionneur complet est une fonction f : 2 3 ? 2 2 telle que si f (x, y, z) = (u, w) alors u est la somme (modulo 2) de x, y et z et w est la retenue de la somme. (1) Représentez la fonction f par deux BDD réduits
, b n ) ? 2 n | f ? (b 1, vol.1
, On se limiterà a faire quelques remarquesélémentairesremarquesélémentaires.-Les 3 méthodes sont sensiblesàsensiblesà l'ordre des variables.-Pour chaque méthode, on peut formuler desprobì emes qui prennent un temps exponentiel pour n'importe quel ordre des variables.-Les 3 méthodes visent des questions (réfutation, satisfaisabilité, ´ equivalence logique) et des domaines d'application (déduction automatique, optimisation combinatoire, vérification de circuits) différents. Par exemple, si on veut comparer résolution et DP il faut plutôt considérer des formules qui ne sont pas satisfaisables (voir, par exemple, Conclusion En conclusion, on peut se demander quelle méthode il convient de choisir parmi celles discutées dans ce cours (résolution, DP et BDD)
, Avec la méthode DP on a une borne linéaire sur la taille des données qu'il faut traiter ce qui n'est pas le cas pour résolution et BDD (avec ces 2 méthodes on peut assez rapidementépuiserrapidementépuiser la mémoire)
, formule ou BDD) jusqu'` a arriveràarriverà une forme o` u la solution est manifeste, par contre la méthode DP procède par une approche de séparation etévaluationetévaluation.-Les meilleurs algorithmes utilisent un certain nombre d'heuristiques (par exemple, dans le choix de la variablè a traiter) dont la présentation est omise.-On trouve de nombreuses méthodes pour la satisfaisabilité qui raffinent la méthode DP mais il est bon de savoir qu'on trouve aussi une classe de méthodes qui s'appuient sur des méthodes probabilistes (marches aléatoires) qui ne, Les méthodes par résolution et par BDD procèdent par transformation de la contrainte
, Mathematical logic for computer science, 2012.
, The efficiency of resolution and Davis-Putnam procedures, SIAM J. Comput, vol.31, issue.4, pp.1048-1075, 2002.
, Term rewriting and all that, 1999.
, Graph-based algorithms for boolean function manipulation, IEEE Trans. Computers, vol.35, issue.8, pp.677-691, 1986.
, On the complexity of VLSI implementations and graph representations of Boolean functions with applications to integer multiplication, IEEE Trans. Computers, vol.40, pp.205-213, 1991.
, A machine program for theorem proving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.
, A computing procedure for quantification theory, J. ACM, vol.7, issue.3, pp.201-215, 1960.
, UntersuchungenüberUntersuchungen¨Untersuchungenüber das logische Schließen I, Mathematische Zeitschrift, vol.39, issue.2, pp.176-210, 1934.
, UntersuchungenüberUntersuchungen¨Untersuchungenüber das logische Schließen II, Mathematische Zeitschrift, vol.39, issue.3, pp.405-431, 1935.
DOI : 10.1007/bf01201363
, Proof theory and automated deduction, 1997.
, The intractability of resolution, Theor. Comput. Sci, vol.39, pp.297-308, 1985.
DOI : 10.1016/0304-3975(85)90144-6
URL : https://doi.org/10.1016/0304-3975(85)90144-6
, The art of computer programming, Combinatorial algorithsms, Part, vol.4, 2012.
, The art of computer programming, Combinatorial algorithms, vol.4, 2018.
, Probability and computing : randomized algorithms and probabilistic analysis, 2005.
, A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.
, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, Part II, pp.115-125, 1970.
, Ordered binary decision diagrams and the Davis-Putnam procedure, Constraints in Computational Logics, First International Conference, CCL'94, pp.34-49, 1994.
, A theorem on boolean matrices, J. ACM, vol.9, issue.1, pp.11-12, 1962.
DOI : 10.1145/321105.321107