Yes the BDD is minimized with the two rules (reduction and elimination). Also the sorting of the boolean functions is optimized via plain brute forcing.

The was no good JavaScript implementation for BDDs so I had to create my own one https://github.com/pubkey/binary-decision-diagram

Cool, I've checked your code and it's not zero suppressed BDDs, although it might not be a performance gain if you used ZDDs. (zero supressed BDDs are very good at representing sets of permutations/combinations etc. but as far as I understand you have all the possible permutations encoded in the BDD, not a subset of all possible permutations).