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

arXiv:2404.12184 · ACM/IEEE Design Automation Conference (DAC)

Boolean Matching Reversible Circuits: Algorithm and Complexity

Tian-Fu Chen, Jie-Hong Roland Jiang

Published Jun 23, 2024• 4 citations
arXivHTMLPDF

Abstract

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.

DOI
10.1145/3649329.3657312

Related papers

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

M. Vénere, Alessandro Barenghi, Gerardo Pelosi

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.

IEEE Transactions on Quantum Engineering•Jan 1, 2025•0 citations

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

Reversible Circuit Realizations of Boolean Functions

Alex Brodsky

Reversible circuits are a concrete model of reversible computation with applications in areas such as quantum computing and analysis of cryptographic block cyphers. In 1980, Toffoli showed how to realize a Boolean function by a reversible circuit, however the resulting complexity of such circuits has remained an open problem. We investigate the reversible circuit complexity of families of Boolean functions and derive conditions that characterize whether a polynomial realization is possible. First, we derive sufficient conditions on families of Boolean functions that guarantee a polynomial-size reversible circuit realization. Namely, we show that if a Boolean function can be embedded into an even parity permutation that has a polynomial-size cycle representation, then the Boolean function can be realized by a polynomial-size reversible circuit. Furthermore, we provide a construction for the realization. Second, we provide concrete realizations for several families of Boolean functions, such as the adder, incrementor, and threshold functions, which do not necessarily satisfy the preceding condition, but still have polynomial-size realizations; this is important because such realizations will necessarily form the building blocks of quantum computers.

Kluwer Academic Publishers eBooks•Feb 21, 2006•5 citations

Quantum logic synthesis by symbolic reachability analysis

William N. N. Hung, Xiaoyu Song B, Guowu Yang +2 more

Reversible quantum logic plays an important role in quantum computing. In this paper, we propose an approach to optimally synthesize quantum circuits by symbolic reachability analysis where the primary inputs are purely binary. we use symbolic reachability analysis, a technique most commonly used in model checking (a way of formal verification), to synthesize the optimum quantum circuits. We present an exact synthesis method with optimal quantum cost and a speedup method with non-optimal quantum cost. Both our methods guarantee the synthesizeability of all reversible circuits. Unlike previous works which use permutative reversible gates, we use a lower level library which includes non-permutative quantum gates. For the first time, problems in quantum logic synthesis have been reduced to those of multiple-valued logic synthesis thus reducing the search space and algorithm complexity. We synthesized quantum circuits for gate, half-adder, full-adder, etc. with the smallest cost.. Our approach obtains the minimum cost quantum circuits for Miller's gate, half-adder, and full-adder, which are better than previous results. In addition, we prove the minimum quantum cost (using our elementary quantum gates) for Fredkin, Peres, and Toffoli gates. Our work constitutes the first successful experience of applying satisfiability with formal methods to quantum logic synthesis.

ACM/IEEE Design Automation Conference (DAC)•Jun 7, 2004•83 citations

Quantum switching and quantum string matching

Tien-Sheng Lin, Chin-Yung Lu, Sy‐Yen Kuo

Applications of quantum string matching can be found in quantum signature scheme and quantum fingerprinting. The major benefit of these applications is computation complexity. Quantum Boolean circuits can check the equivalence function: all in puts are quantum digital state. However, it is difficult to verify quantum strings if all input qubits are quantum superposition state. Quantum switching could be reversible circuits. These circuits have two major benefits: information lossless and energy saving. In this paper, we use quantum circuits to design the control module that can verify the equivalence of quantum strings and satisfy the following condition: all inputs qubits could be quantum superposition state. In the pro posed circuits, the control module can form a special correlation between input sequence and output sequence. This correlation can design the equivalence function of quantum strings to solve the problem: input strings with superposition. In regard to the performance, the scalability of the proposed circuits can be achieved.

IEEE International Conference on Nanotechnology (IEEE-NANO)•Aug 1, 2010•6 citations

Optimized Boolean expression embedding in quantum and reversible logic circuits

Zaid Al-Wardi

The quantum and reversible circuits represent a promising replacement of conventional computers in many applications in the future. The transition between conventional computing and this alternative is indeed a huge paradigm shift. During the transition, embedding of conventional Boolean logic functions and expressions within quantum and reversible logic circuits has to be considered, because conventional computing is generally based on Boolean algebra. This embedding comes with a serious drawback of additional increase in the problem complexity represented by additional constant inputs, the so-called ancillary lines. An algorithmic optimization technique is suggested in this paper to reduce the number of these ancillary lines. With this algorithm embedding of Boolean expressions within reversible/quantum circuits comes out with minimal increase in circuit cost and gate count in the optimized circuits.

AIP conference proceedings•Jan 1, 2023•0 citations
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.
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.
Reversible circuits are a concrete model of reversible computation with applications in areas such as quantum computing and analysis of cryptographic block cyphers. In 1980, Toffoli showed how to realize a Boolean function by a reversible circuit, however the resulting complexity of such circuits has remained an open problem. We investigate the reversible circuit complexity of families of Boolean functions and derive conditions that characterize whether a polynomial realization is possible. First, we derive sufficient conditions on families of Boolean functions that guarantee a polynomial-size reversible circuit realization. Namely, we show that if a Boolean function can be embedded into an even parity permutation that has a polynomial-size cycle representation, then the Boolean function can be realized by a polynomial-size reversible circuit. Furthermore, we provide a construction for the realization. Second, we provide concrete realizations for several families of Boolean functions, such as the adder, incrementor, and threshold functions, which do not necessarily satisfy the preceding condition, but still have polynomial-size realizations; this is important because such realizations will necessarily form the building blocks of quantum computers.
Reversible quantum logic plays an important role in quantum computing. In this paper, we propose an approach to optimally synthesize quantum circuits by symbolic reachability analysis where the primary inputs are purely binary. we use symbolic reachability analysis, a technique most commonly used in model checking (a way of formal verification), to synthesize the optimum quantum circuits. We present an exact synthesis method with optimal quantum cost and a speedup method with non-optimal quantum cost. Both our methods guarantee the synthesizeability of all reversible circuits. Unlike previous works which use permutative reversible gates, we use a lower level library which includes non-permutative quantum gates. For the first time, problems in quantum logic synthesis have been reduced to those of multiple-valued logic synthesis thus reducing the search space and algorithm complexity. We synthesized quantum circuits for gate, half-adder, full-adder, etc. with the smallest cost.. Our approach obtains the minimum cost quantum circuits for Miller's gate, half-adder, and full-adder, which are better than previous results. In addition, we prove the minimum quantum cost (using our elementary quantum gates) for Fredkin, Peres, and Toffoli gates. Our work constitutes the first successful experience of applying satisfiability with formal methods to quantum logic synthesis.
Applications of quantum string matching can be found in quantum signature scheme and quantum fingerprinting. The major benefit of these applications is computation complexity. Quantum Boolean circuits can check the equivalence function: all in puts are quantum digital state. However, it is difficult to verify quantum strings if all input qubits are quantum superposition state. Quantum switching could be reversible circuits. These circuits have two major benefits: information lossless and energy saving. In this paper, we use quantum circuits to design the control module that can verify the equivalence of quantum strings and satisfy the following condition: all inputs qubits could be quantum superposition state. In the pro posed circuits, the control module can form a special correlation between input sequence and output sequence. This correlation can design the equivalence function of quantum strings to solve the problem: input strings with superposition. In regard to the performance, the scalability of the proposed circuits can be achieved.
The quantum and reversible circuits represent a promising replacement of conventional computers in many applications in the future. The transition between conventional computing and this alternative is indeed a huge paradigm shift. During the transition, embedding of conventional Boolean logic functions and expressions within quantum and reversible logic circuits has to be considered, because conventional computing is generally based on Boolean algebra. This embedding comes with a serious drawback of additional increase in the problem complexity represented by additional constant inputs, the so-called ancillary lines. An algorithmic optimization technique is suggested in this paper to reduce the number of these ancillary lines. With this algorithm embedding of Boolean expressions within reversible/quantum circuits comes out with minimal increase in circuit cost and gate count in the optimized circuits.