Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

IEEE Transactions on Quantum Engineering

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

M. Vénere, Alessandro Barenghi, Gerardo Pelosi

Published Jan 1, 2025• 0 citations
Publisher

Abstract

The Boolean Matching Problem via$NP$-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, thelibrary-mappingstep of an EDA workflow requires matching parts of the gate-level design (netlist) 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$n$-to-$n$vector Boolean functions, where$n$is the number of input and output variables, the search space of possible negations and permutations is super-exponential in size, while the$\mathcal {O}(n!n2^{2n})$time complexity of classical approaches allows solving only small instances of the$NP$-problem, often limited to$n$-to-1 Boolean functions (executing$\mathcal {O}(n!2^{2n})$bit operations). This work presents a quantum algorithm for matching$n$-to-$n$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.

DOI
10.1109/tqe.2025.3595275

Related papers

A Quantum Method to Match Vector Boolean Functions using Simon's Solver

M. Vénere, Alessandro Barenghi, Gerardo Pelosi

The Boolean Matching Problem is a fundamental step in modern Electronic Design Automation toolchains, which allow the efficient design of large classical computers. In particular, the equivalence under negation-permutation-negation of two n-to-n vector Boolean functions requires the exploration of a super-exponential number of possible negations and permutations of input and output variables, and is widely regarded as a daunting challenge. Its classical complexity$(\mathcal{O}(n!2^{2n})$, where$n$is the number of input and output variables) is rarely tolerated by EDA tools, which are typically solving small instances of the Boolean Matching Problem for n-to-1 Boolean functions. In this work, we present a method to exploit the solver for Simon's problem to speedup the matching of n-to-n vector Boolean functions, as we show that, despite its higher complexity, it is friendlier to a quantum solver than matching single-output Boolean functions. Our solution allows saving a factor$2^{n}$in the overall worst-case computational effort, and is amenable to combined approaches such as the so-called Grover-meets-Simon, which have the potential of reducing it below the cost of classical n-to-1 matching. We provide a fully detailed quantum circuit implementing our proposal, and compute its cost, both counting the required amount of qubits and quantum gates. We conducted an experimental evaluation employing the ISCAS benchmark suite, a de-facto standard for classical EDA to derive our sample Boolean functions.

IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD)•Nov 18, 2024•3 citations

Boolean Matching Reversible Circuits: Algorithm and Complexity

Tian-Fu Chen, Jie-Hong Roland Jiang

Boolean matching is an important problem in logic synthesis and verification. Despite being well-studied for conventional Boolean circuits, its treatment for reversible logic circuits remains largely, if not completely, missing. This work provides the first such study. Given two (black-box) reversible logic circuits that are promised to be matchable, we check their equivalences under various input/output negation and permutation conditions subject to the availability/unavailability of their inverse circuits. Notably, among other results, we show that the equivalence up to input negation and permutation is solvable in quantum polynomial time, while its classical complexity is exponential. This result is arguably the first demonstration of quantum exponential speedup in solving design automation problems. Also, as a negative result, we show that the equivalence up to both input and output negations is not solvable in quantum polynomial time unless UNIQUE-SAT is, which is unlikely. This work paves the theoretical foundation of Boolean matching reversible circuits for potential applications, e.g., in quantum circuit synthesis.

arXiv:2404.12184•ACM/IEEE Design Automation Conference (DAC)•Jun 23, 2024•4 citations

From Boolean functions to quantum circuits: A scalable quantum compilation flow in C++

Bruno de O. Schmitt, Fereshte Mozafari, Giulia Meuli +2 more

We propose a flow for automated quantum compilation. Our flow takes a Boolean function implemented in Python as input and translates it into a format appropriate for reversible logic synthesis. We focus on two quantum compilation tasks: uniform state preparation and oracle synthesis. To illustrate the use of our flow, we solve IBM's virtual hackathon challenge of 2019, called the Zed city problem, an instance of vertex coloring, by using quantum search algorithms. The expressiveness of Python in combination with automated compilation algorithms allows us to express quantum algorithms at a high level of abstraction, which reduces the effort to implement them, and leads to better and more flexible implementations. We show that our proposed flow generates a lower-cost circuit implementation of the oracle needed to solve IBM's challenge when compared to the winning submission.

Design, Automation, and Test in Europe•Feb 1, 2021•6 citations

Automated Theorem Proving for Quantum Circuit Verification using SAT Solvers

Jincheng Zhang

The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.

•Sep 5, 2026•0 citations

Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking

Shang-Wei Lin, Ji-Qing Yan, Yean-Ru Chen +2 more

Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.

quant-pharXiv:2604.18218•Apr 21, 2026•0 citations

Synthesis of quantum-logic circuits

Vivek Shende, Stephen S. Bullock, Igor L. Markov

The pressure of fundamental limits on classical computation and the promise of exponential speedups from quantum effects have recently brought quantum circuits (Proc. R. Soc. Lond. A, Math. Phys. Sci., vol. 425, p. 73, 1989) to the attention of the electronic design automation community (Proc. 40th ACM/IEEE Design Automation Conf., 2003), (Phys. Rev. A, At. Mol. Opt. Phy., vol. 68, p. 012318, 2003), (Proc. 41st Design Automation Conf., 2004), (Proc. 39th Design Automation Conf., 2002), (Proc. Design, Automation, and Test Eur., 2004), (Phys. Rev. A, At. Mol. Opt. Phy., vol. 69, p. 062321, 2004), (IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol. 22, p. 710, 2003). Efficient quantum-logic circuits that perform two tasks are discussed: 1) implementing generic quantum computations, and 2) initializing quantum registers. In contrast to conventional computing, the latter task is nontrivial because the state space of an n-qubit register is not finite and contains exponential superpositions of classical bitstrings. The proposed circuits are asymptotically optimal for respective tasks and improve earlier published results by at least a factor of 2. The circuits for generic quantum computation constructed by the algorithms are the most efficient known today in terms of the number of most expensive gates [quantum controlled-NOTs (CNOTs)]. They are based on an analog of the Shannon decomposition of Boolean functions and a new circuit block, called quantum multiplexor (QMUX), which generalizes several known constructions. A theoretical lower bound implies that the circuits cannot be improved by more than a factor of 2. It is additionally shown how to accommodate the severe architectural limitation of using only nearest neighbor gates, which is representative of current implementation technologies. This increases the number of gates by almost an order of magnitude, but preserves the asymptotic optimality of gate counts.

arXiv:quant-ph/0406176•IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems•May 12, 2006•678 citations
The Boolean Matching Problem viaNPNPNP-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, thelibrary-mappingstep of an EDA workflow requires matching parts of the gate-level design (netlist) 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. Fornnn-to-nnnvector Boolean functions, wherennnis the number of input and output variables, the search space of possible negations and permutations is super-exponential in size, while theO(n!n22n)\mathcal {O}(n!n2^{2n})O(n!n22n)time complexity of classical approaches allows solving only small instances of theNPNPNP-problem, often limited tonnn-to-1 Boolean functions (executingO(n!22n)\mathcal {O}(n!2^{2n})O(n!22n)bit operations). This work presents a quantum algorithm for matchingnnn-to-nnnvector 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.
The Boolean Matching Problem is a fundamental step in modern Electronic Design Automation toolchains, which allow the efficient design of large classical computers. In particular, the equivalence under negation-permutation-negation of two n-to-n vector Boolean functions requires the exploration of a super-exponential number of possible negations and permutations of input and output variables, and is widely regarded as a daunting challenge. Its classical complexity(O(n!22n)(\mathcal{O}(n!2^{2n})(O(n!22n), wherennnis the number of input and output variables) is rarely tolerated by EDA tools, which are typically solving small instances of the Boolean Matching Problem for n-to-1 Boolean functions. In this work, we present a method to exploit the solver for Simon's problem to speedup the matching of n-to-n vector Boolean functions, as we show that, despite its higher complexity, it is friendlier to a quantum solver than matching single-output Boolean functions. Our solution allows saving a factor2n2^{n}2nin the overall worst-case computational effort, and is amenable to combined approaches such as the so-called Grover-meets-Simon, which have the potential of reducing it below the cost of classical n-to-1 matching. We provide a fully detailed quantum circuit implementing our proposal, and compute its cost, both counting the required amount of qubits and quantum gates. We conducted an experimental evaluation employing the ISCAS benchmark suite, a de-facto standard for classical EDA to derive our sample Boolean functions.
Boolean matching is an important problem in logic synthesis and verification. Despite being well-studied for conventional Boolean circuits, its treatment for reversible logic circuits remains largely, if not completely, missing. This work provides the first such study. Given two (black-box) reversible logic circuits that are promised to be matchable, we check their equivalences under various input/output negation and permutation conditions subject to the availability/unavailability of their inverse circuits. Notably, among other results, we show that the equivalence up to input negation and permutation is solvable in quantum polynomial time, while its classical complexity is exponential. This result is arguably the first demonstration of quantum exponential speedup in solving design automation problems. Also, as a negative result, we show that the equivalence up to both input and output negations is not solvable in quantum polynomial time unless UNIQUE-SAT is, which is unlikely. This work paves the theoretical foundation of Boolean matching reversible circuits for potential applications, e.g., in quantum circuit synthesis.
We propose a flow for automated quantum compilation. Our flow takes a Boolean function implemented in Python as input and translates it into a format appropriate for reversible logic synthesis. We focus on two quantum compilation tasks: uniform state preparation and oracle synthesis. To illustrate the use of our flow, we solve IBM's virtual hackathon challenge of 2019, called the Zed city problem, an instance of vertex coloring, by using quantum search algorithms. The expressiveness of Python in combination with automated compilation algorithms allows us to express quantum algorithms at a high level of abstraction, which reduces the effort to implement them, and leads to better and more flexible implementations. We show that our proposed flow generates a lower-cost circuit implementation of the oracle needed to solve IBM's challenge when compared to the winning submission.
The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.
Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.
The pressure of fundamental limits on classical computation and the promise of exponential speedups from quantum effects have recently brought quantum circuits (Proc. R. Soc. Lond. A, Math. Phys. Sci., vol. 425, p. 73, 1989) to the attention of the electronic design automation community (Proc. 40th ACM/IEEE Design Automation Conf., 2003), (Phys. Rev. A, At. Mol. Opt. Phy., vol. 68, p. 012318, 2003), (Proc. 41st Design Automation Conf., 2004), (Proc. 39th Design Automation Conf., 2002), (Proc. Design, Automation, and Test Eur., 2004), (Phys. Rev. A, At. Mol. Opt. Phy., vol. 69, p. 062321, 2004), (IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol. 22, p. 710, 2003). Efficient quantum-logic circuits that perform two tasks are discussed: 1) implementing generic quantum computations, and 2) initializing quantum registers. In contrast to conventional computing, the latter task is nontrivial because the state space of an n-qubit register is not finite and contains exponential superpositions of classical bitstrings. The proposed circuits are asymptotically optimal for respective tasks and improve earlier published results by at least a factor of 2. The circuits for generic quantum computation constructed by the algorithms are the most efficient known today in terms of the number of most expensive gates [quantum controlled-NOTs (CNOTs)]. They are based on an analog of the Shannon decomposition of Boolean functions and a new circuit block, called quantum multiplexor (QMUX), which generalizes several known constructions. A theoretical lower bound implies that the circuits cannot be improved by more than a factor of 2. It is additionally shown how to accommodate the severe architectural limitation of using only nearest neighbor gates, which is representative of current implementation technologies. This increases the number of gates by almost an order of magnitude, but preserves the asymptotic optimality of gate counts.