Functional Symmetries and Their Uses in Optimization and Verification
Donald Chai and Andreas Kuehlmann
Symmetries of (Boolean) functions are transformations of the inputs which do not modify the output under any assignment of values to the inputs. Classically, the transformations considered are swaps of individual variables, whereas in this work, we shall consider arbitrary permutations of the inputs, as well as the possibility of negating inputs. Furthermore, in our work we consider circuits consisting of multiple levels of logic gates; in this case, permutation may occur anywhere within the circuit, not only at its inputs.
Knowledge of symmetries allows us to enlarge the design space for various optimization problems, and shrink the search space for others. This research explores applications in technology mapping for timing optimization, placement, and verification.