Generalized Affine Equivalence Checking of Boolean Functions via Reachability Analysis

We consider the problem of checking the generalized affine equivalence of two given Boolean functions. This problem arises in various computer-aided design (CAD) and cryptographic applications, such as circuit synthesis and Reed-Muller codes. Based on the theory of affine group acting on the Boolean functions, we define the coefficient spaces and transition relations, and transform the checking problem into reachability analysis of finite state machines. Two methods are proposed to check the affine equivalence of Boolean functions using binary decision diagrams (BDDs) and property directed reachability (PDR), respectively. Both methods can check affine equivalence of bent and semi-bent functions, which state-of-the-art methods can hardly handle. Furthermore, existing methods only consider the case of affine equivalence, while our methods can handle the generalized affine equivalence of subspaces of Boolean functions. In the application of circuit synthesis, our methods can significantly reduce the size of the library compared to Boolean matching. To classify Boolean functions up to the generalized affine equivalence, we propose a method to obtain a complete classification based on BDDs. In the experiments, we have successfully applied our methods to some examples that can hardly be solved by using the previous methods, thus, validating the effectiveness of our methods.