Symbolic Execution of the Quine-McCluskey Algorithim If I understand correctly, the Quine–McCluskey algorithm will find the minimum boolean formula size for given boolean function.  Has there been any attempts to (for lack of a better term) symbolically execute the algorithm with a class of boolean functions rather than a single one to find a circuit unconditional lower bound?  Just curious to see if anybody has tried this before, and if so,(presumably) why it wouldn't work.

https://en.wikipedia.org/wiki/Symbolic_execution
Since you stated your purpose is considering circuit bounds:

Taking a boolean function and "minimizing" using Karnaugh maps or the Quine–McCluskey algorithm, then converting the formula to AND and OR gates will give you a circuit calculating that function.  This however does not actually give you a minimum sized circuit.  Karnaugh maps minimize the number of product terms in the sum of products form of specifying a function, this is NOT the same as minimizing the number of gates in a circuit.

Consider for instance the $N$ input parity function. The sum of products form will have $2^{N-1}$ minterms, which means you'd need an exponential number of gates using this method.  However if it takes us $M$ of whatever gates are your basis to make a 2-input XOR gate, we can make the $N$ input parity function with only $M(N-1)$ gates: a linear bound.