, Quand toutes ces optimisations sont mises en oeuvre etétant donné une table d'hachage qui garantit un temps d'accès constant en moyenne, il est possible de montrer que la complexité de l'opération d'application est de l'ordre du produit de la taille des BDD reçus en entrée. En gros, une opération logique peut au plusélever au carré la taille de la représentation ; on appelle cela une propriété de dégradation gracieuse. Bien sûr, l'itération d'un carré donne un exponentiel, fois qu'on arriveà 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

, Exercice 81 Utilisez l'algorithme A pour construire un BDD réduit qui définit la fonction : AND(NOR(x, y), AND(z, w))

, Exercice 82 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

, Exercice 83 Proposez un algorithme qui prend un BDD ? par rapport aux variables or

.. .. =-{(b-1, b n ) ? 2 n | f ? (b 1, vol.1

, Bornes inférieures On introduit des techniques pour montrer une borne inférieure exponentielle sur la taille d'un BDD réduit qui calcule certaines fonctions. Ces techniques peuvent sembler un peu ad hoc mais sont en réalité des spécimens d'une théorie connue comme complexité de la communication ; une branche de la théorie de la complexité du calcul qui est souvent utilisée pourétablir des bornes inférieures

, b n ) où b i ? 2 il existe unique un chemin dans ? qui commenceà la racine de ? et progresse en se basant sur l'affectation v = [b 1 /x 1 , . . . , b n /x n ] jusqu'à arriverà un noeud n(?, v), la fonction f par rapportà cet ordre. Pour toute tuple

, le BDD doit retourner 1 pour l'affectation v

, On aborde maintenant la fonction h (6.2) de la section 6.2 (la hidden weighted bit function)

, Exercice 87 Montrez que la fonction h n'est pas symétrique

, Exercice 88 Soient f : 2 n ? 2 et g : 2 m ? 2 deux fonctions telles que n < m et pour toute entrée b 1

.. .. +-?-j=m+1, b m /x m ] pour m < n. de v ? Une solution pourraitêtre de faire en sorte que : ? j=1, On considère d'abord l'ordre x 1 < · · · < x n et on chercheà adapter l'argument utilisé pour la fonction f en considérant des affectations de la forme

, Par exemple, si i = 1 alors on force k = 1 et le nombre d'affectations possibles est linéaire en n. Il faut donc que le i ne soit pas trop petit

M. Ben-ari, Mathematical logic for computer science, 2012.

P. Beame, R. M. Karp, T. Pitassi, and M. E. Saks, The efficiency of resolution and Davis-Putnam procedures, SIAM J. Comput, vol.31, issue.4, pp.1048-1075, 2002.

F. Baader and T. Nipkow, Term rewriting and all that, 1999.

R. E. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Trans. Computers, vol.35, issue.8, pp.677-691, 1986.

R. E. Bryant, 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.

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem proving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.

M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM, vol.7, issue.3, pp.201-215, 1960.

G. Gentzen, Untersuchungenüber das logische Schließen I, Mathematische Zeitschrift, vol.39, issue.2, pp.176-210, 1934.

G. Gentzen, Untersuchungenüber das logische Schließen II, Mathematische Zeitschrift, vol.39, issue.3, pp.405-431, 1935.

J. Goubault, -. Larrecq, and I. Mackie, Proof theory and automated deduction, 1997.

A. Haken, The intractability of resolution, Theor. Comput. Sci, vol.39, pp.297-308, 1985.

E. Kushilevitz and N. Nisan, Communication complexity, 1997.

D. Knuth, The art of computer programming, Combinatorial algorithsms, Part, vol.4, 2012.

D. Knuth, The art of computer programming, Combinatorial algorithms, vol.4, 2018.

M. Mitzenmacher and E. Upfal, Probability and computing : randomized algorithms and probabilistic analysis, 2005.

R. John-alan, A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.

G. Tseitin, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, Part II, pp.115-125, 1970.

E. Tomás, M. E. Uribe, and . Stickel, Ordered binary decision diagrams and the Davis-Putnam procedure, Constraints in Computational Logics, First International Conference, CCL'94, pp.34-49, 1994.

S. Warshall, A theorem on boolean matrices, J. ACM, vol.9, issue.1, pp.11-12, 1962.