I saw the proof in some Binary-decision-diagram book that I've forgotten the name of.
The gist is that if you have a symmetric function (ie: order doesn't matter) of say, 8-bits, then that means f(10101010) == f(11110000) == f(00001111), and all such combinations. Because this is the very definition of "order doesn't matter".
This necessarily implies that f(bits) can be rewritten into the form of f(bits) == g(popcnt(bits)).
Something to do with counting up all the possibilities of "order doesn't matter" and then pigeon-holing them into popcnt combinations or something really mathematical like that. I'm sorry I don't remember the proof, but hopefully this is enough to give you the gist of the idea.
------------------
For example: XOR is the simplest symmetric function. We can see that XOR can be rewritten as XOR(bits) == g(popcnt(bits)). Where G is "take the bottom-bit from popcnt".
A lot of the "power" of BDDs is their ability to uncannily decompose functions into symmetric and non-symmetric parts. Not consistently mind you, but if a BDD is well-behaved (low-memory space, high-speeds, etc. etc.), its likely because a large part of the calculations happened to be symmetric.
This can be beneficial with say addFourDWORDs(a, b, c, d), where a+b+c+d has a "partial" level of symmetry. (a_0 XOR b_0 XOR c_0 XOR d_0 determines output_0 bit... while the 1st bit is related to XOR (a1,b1,c1,d1), etc. etc.). So there's all kinds of 'hidden popcounts" that could pop up in practice for random functions (IE: "partially symmetric"), though its a puzzle on how to exactly decompose arbitrary bit-functions into this form.
And even if you do, its no guarantee that the popcnt form was actually faster either. But it does give you some "trick" to try when trying to optimize an arbitrary bitwise function into a high-speed routine.
-----------------
Other symmetric functions (assuming 8-bit numbers)
The gist is that if you have a symmetric function (ie: order doesn't matter) of say, 8-bits, then that means f(10101010) == f(11110000) == f(00001111), and all such combinations. Because this is the very definition of "order doesn't matter".
This necessarily implies that f(bits) can be rewritten into the form of f(bits) == g(popcnt(bits)).
Something to do with counting up all the possibilities of "order doesn't matter" and then pigeon-holing them into popcnt combinations or something really mathematical like that. I'm sorry I don't remember the proof, but hopefully this is enough to give you the gist of the idea.
------------------
For example: XOR is the simplest symmetric function. We can see that XOR can be rewritten as XOR(bits) == g(popcnt(bits)). Where G is "take the bottom-bit from popcnt".
A lot of the "power" of BDDs is their ability to uncannily decompose functions into symmetric and non-symmetric parts. Not consistently mind you, but if a BDD is well-behaved (low-memory space, high-speeds, etc. etc.), its likely because a large part of the calculations happened to be symmetric.
This can be beneficial with say addFourDWORDs(a, b, c, d), where a+b+c+d has a "partial" level of symmetry. (a_0 XOR b_0 XOR c_0 XOR d_0 determines output_0 bit... while the 1st bit is related to XOR (a1,b1,c1,d1), etc. etc.). So there's all kinds of 'hidden popcounts" that could pop up in practice for random functions (IE: "partially symmetric"), though its a puzzle on how to exactly decompose arbitrary bit-functions into this form.
And even if you do, its no guarantee that the popcnt form was actually faster either. But it does give you some "trick" to try when trying to optimize an arbitrary bitwise function into a high-speed routine.
-----------------
Other symmetric functions (assuming 8-bit numbers)
AND(bits) == (popcnt(bits) == 8).
OR(bits) == (popcnt(bits) > 0)
Etc. etc.
EDIT: Looks like Wikipedia has a link to this concept: https://en.wikipedia.org/wiki/Symmetric_Boolean_function