Efficient method for generating the smoothing function
Suppose that we are substituting variable $x$.

You will have a lot of zeroes and ones in the circuit, so a simple simplification function should help a lot. Additionally a potentially large part of your circuit unrelated to $x$ might be duplicated, so I would suggest preventing its duplication in the first place.

First I would mark any inputs (including the constants $0$ and $1$) to the circuit that aren't $x$ as unrelated. Second, any gate that only has unrelated inputs is marked as unrelated itself. This is done repeatedly until the result is stable. Then, any unrelated subcircuit which has a related gate as parent is removed and replaced with a temporary variable (e.g. $t_1, t_2,$ etc) and it is for each temporary variable what circuit it corresponded to.

Then you should apply your smoothing function definition and minimize recursively using $S$, applying matching with priority from top to bottom:

$$\begin{align}
S(0) &amp;= 0\\
S(1) &amp;= 1\\
S(\neg 0) &amp;= 1\\
S(\neg 1) &amp;= 0\\
S(a + b) &amp;= \begin{cases}
    1 &amp; S(a) = 1 \vee S(b) = 1\\
    0 &amp; S(a) = 0 \wedge S(b) = 0\\
    S(a) &amp; S(b) = 0\\
    S(b) &amp; S(a) = 0\\
    S(a) &amp; S(a) = S(b)\\
    S(a) + S(b)&amp;S(a) &lt; S(b)\\
    S(b) + S(a)&amp;\text{otherwise}
\end{cases}\\
S(a \cdot b) &amp;=\begin{cases}
    1 &amp; S(a) = 1 \wedge S(b) = 1\\
    0 &amp; S(a) = 0 \vee S(b) = 0\\
    S(a) &amp; S(b) = 1\\
    S(b) &amp; S(a) = 1\\
    S(a) &amp; S(a) = S(b)\\
    S(a) \cdot S(b)&amp; S(a) &lt; S(b)\\
    S(b) \cdot S(a)&amp; \text{otherwise}\\
\end{cases}\\
S(\neg \neg a) &amp;= S(a)\\
S(\neg a) &amp;= \neg S(a)\\
S(a) &amp;= a\end{align}$$

Note that all comparisons here are done simply on the symbolic formulas, with comparison done in any consistent order (such as an arbitrary lexicographic order). This minimization isn't very advanced, but runs very fast and fully eliminates any constants unless the entire circuit is constant. If your primitive gates aren't conjunction and disjunction you'll need a different minimization function, but I think the concept is clear.

After minimization is done you can add back the $t_1, t_2,$etc circuits and connect wherever they occur.



Practical algorithms aside, I don't believe that your intuition of the circuit becoming simpler is correct when truth tables are too large to be enumerated.

Let's do a napkin math calculation. Suppose you have 64 inputs and consider a 'reasonable' useful circuit any circuit with $\leq 10000$ binary gates, then there are $4\sum_{g=0}^{10000}\sum_{k=0}^{g} (64+k)^2$ possible circuits, assuming $4$ different gate types. That's approximately $2^{52}$ possible reasonably sized circuits.

There are $2^{2^{64}}$ possible truth tables. We haven't even scratched the surface of the surface of all possible circuits. There is plenty of space for combinations of reasonable circuits to blow up exponentially in size and I don't see reason to believe why they wouldn't - there's plenty of domain left to blow up into.