A Grover-Meets-Simon Approach to Match Vector Boolean Functions

The Boolean Matching Problem via <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$NP$</tex-math></inline-formula>-Equivalence requires determining whether two Boolean functions are equivalent or not up to a permutation and negation of the input binary variables. Its solution is a fundamental step in the Electronic Design Automation (EDA) tool chains commonly used for digital circuit design. In fact, the <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">library-mapping</i> step of an EDA workflow requires matching parts of the gate-level design (<italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">netlist</i>) with the components available in a technology library, considering them as Boolean functions, while taking into account that permutations and negations of input variables can be efficiently implemented through rewiring and the use of inverters. For <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$n$</tex-math></inline-formula>-to-<inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$n$</tex-math></inline-formula> vector Boolean functions, where <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$n$</tex-math></inline-formula> is the number of input and output variables, the search space of possible negations and permutations is super-exponential in size, while the <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\mathcal {O}(n!n2^{2n})$</tex-math></inline-formula> time complexity of classical approaches allows solving only small instances of the <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$NP$</tex-math></inline-formula>-problem, often limited to <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$n$</tex-math></inline-formula>-to-1 Boolean functions (executing <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\mathcal {O}(n!2^{2n})$</tex-math></inline-formula> bit operations). This work presents a quantum algorithm for matching <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$n$</tex-math></inline-formula>-to-<inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$n$</tex-math></inline-formula> vector Boolean functions by effectively combining the Grover-meets-Simon approach with an original and novel use of the Simon solver without the constraints imposed by its usual premises. We provide a fully detailed quantum circuit implementing our proposal, calculate its cost by evaluating key performance indicators for circuit synthesis and show an exponential speedup over classical solutions. Finally, we validate our approach on the Boolean functions included in the ISCAS benchmark suite, which are of practical interest in EDA.