Generalized Boolean symmetries through nested partition refinement

Combinatorial objects in EDA applications exhibit a great amount of complexity and typically defy polynomial-time algorithms. To achieve acceptable performance, EDA tools seek to exploit various structures found in these objects in practice. In this work, we explore symmetries of Boolean functions and develop a new algorithm based on nested partition refinement, abstract group theory and Boolean satisfiability. We apply our algorithm to solve large-scale Boolean matching.