# 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

• a/the main issue or way to visualize this is the algorithm doesnt give you a (nontrivial) DAG, its a tree. most lower bounds are questions about DAGs. – vzn Jul 5 '15 at 5:33

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.