Number of unique outputs by substituting variables
Mathematica, O(k^2(k!)^2) time
Length[Union@@(Fold[Flatten[{StringReplace[#,#2-&gt;&quot;0&quot;],StringReplace[#,#2-&gt;&quot;1&quot;]}]&amp;,#,Union[Characters[#]]]&amp;/@#)]&amp;

Hopefully I calculated the time complexity correctly. Input is a list of formulas such as {&quot;bacb&quot;,&quot;bcab&quot;,&quot;cbba&quot;,&quot;abbc&quot;}. Runs in less than 30 seconds for every test case on my machine, but who cares about absolute times?
Explanation:

First off, the &amp; at the end makes it a pure function, with # referring to the first argument, #2 being the second argument, etc.
Length[*..*] takes the length of the list contained inside it.
Union@@(*..*) takes the contained list and supplies it as the arguments for Union, which returns a list of the unique elements in any of its arguments.
*..*&amp;/@# takes a pure function and maps it over the list of formulas, so that {a,b,c} becomes {f[a],f[b],f[c]}. Note that in nested pure functions, #n refers to its innermost arguments.
Fold[*..*&amp;,#,*..*] takes a accumulator function, starting value, and list, and returns f[f[...[f[starting value,l_1],l_2],...],l_n].
Union[Characters[#]] takes all the characters in the current formula and gets all the unique elements, giving us the variables.
Flatten[*..*] flattens its argument, so that {{{a},b},{{c,{d}}}} becomes {a,b,c,d}.
{*..*,*..*} is simply a way to combine the two results using the above Flatten.
StringReplace[#,#2-&gt;&quot;0/1&quot;] takes the previous result and returns it with the current variable replaced with either 0 or 1.