

A040996


Maximum number of distinct functions at the bottom of a Boolean (or Binary) Decision Diagram (or BDD) with negation by pointer complementation.


1



1, 6, 120, 32640, 2147450880, 9223372034707292160, 170141183460469231722463931679029329920, 57896044618658097711785492504343953926464851149359812787997104700240680714240
(list;
graph;
refs;
listen;
history;
text;
internal format)



OFFSET

0,2


COMMENTS

At 0, the last variable, the only choice is (t, f) because the first entry is always uncomplemented and the 2nd must be different.
At level 1, the 2nd to last variable, the first entry is either t or a pointer to a following level (0) and the 2nd entry is either of these or its negation, except it may not equal the first entry.
At level n, the nth to last variable, the first entry is either t or a pointer to one of the following levels' functions and the second entry is any of these or its negation, but not equal to the first entry.


REFERENCES

Cezar Campeanu, Nelma Moreira, Rogerio Reis, Expected Compression Ratio for DFCA: experimental average case analysis, Technical Report Series: DCC201107, December 2011, Departamento de Ciencia de Computadores, Universidade do Porto; http://www.dcc.fc.up.pt/dcc/Pubs/TReports/TR11/dcc201107.pdf


LINKS

Vincenzo Librandi, Table of n, a(n) for n = 0..12
David L. Dill, Higherlevel verification with BDDs


FORMULA

a(n) = (S(n1) + 1) * (2*S(n1) + 1) where S(n1) = Sum_{k<n} a(k).
a(n) is the (2^(2^n)1)th triangular number; i.e., a(n) = 2^(2^n)*(2^(2^n)1)/2.


MATHEMATICA

f[x_]:=Module[{c=2^(2^x)}, (c(c1))/2]; Array[f, 10, 0] (* Harvey P. Dale, Sep 29 2011 *)


PROG

(PARI) a(n)=if(n<=0, n==0, 2^(2^n)*(2^(2^n)1)/2)
(MAGMA) [2^(2^n)*(2^(2^n)1)/2: n in [0..10]]; // Vincenzo Librandi, Sep 30 2011


CROSSREFS

Sequence in context: A053777 A023199 A007539 * A110442 A137149 A317888
Adjacent sequences: A040993 A040994 A040995 * A040997 A040998 A040999


KEYWORD

nonn


AUTHOR

R. H. Hardin


STATUS

approved



