Reversible logic synthesis is a crucial component in quantum electronic design automation. While rule-based methodologies have gained prominence in reversible circuit optimization, the completeness of the transformation rule systems is a longstanding problem in this domain. In this work, we propose the first complete set of transformation rules for reversible circuits, comprising five fundamental rules: any two equivalent reversible circuits can be transformed into each other using the rules. To prove the completeness, a canonical circuit representation for reversible functions is introduced, and we show that every reversible function is computed by a unique reversible circuit in the canonical form, and any reversible circuit can be transformed into its canonical form by applying the rules.
Transformation rules play a central role in reversible circuit optimization, template-based rewriting, and equivalence checking, and establishing their completeness is a fundamental problem in reversible logic synthesis. In this work, we investigate the completeness of transformation rules for reversible circuits both with and without ancillary bits and garbage outputs. For reversible circuits without ancillary bits and garbage outputs, we introduce a refined and complete transformation rule set
RCr, obtained by replacing one rule in the rule set
RC proposed in the previous work (TCAD, 45, pp. 3711--3724, 2026) with a simpler and widely adopted transformation rule. Since all rules in
RCr are commonly used in reversible logic synthesis, this result reveals that practically adopted transformation rules are already sufficient to establish a complete rewriting framework. Based on this result, we further propose an extended rule set, denoted by
RC+, and prove its completeness for reversible circuits with ancillary bits and garbage outputs. To the best of our knowledge, this work presents the first complete transformation rule set for arbitrary reversible circuits, regardless of whether ancillary bits or garbage outputs are employed. The proposed framework establishes a theoretical foundation for circuit optimization, template generation, and equivalence checking, and may facilitate the development of automated design tools for reversible and quantum circuits.
Reversible logic circuits have been historically motivated by theoretical research in low-power electronics as well as practical improvement of bit manipulation transforms in cryptography and computer graphics. Recently, reversible circuits have attracted interest as components of quantum algorithms, as well as in photonic and nano-computing technologies where some switching devices offer no signal gain. Research in generating reversible logic distinguishes between circuit synthesis, postsynthesis optimization, and technology mapping. In this survey, we review algorithmic paradigms—search based, cycle based, transformation based, and BDD based—as well as specific algorithms for reversible synthesis, both exact and heuristic. We conclude the survey by outlining key open challenges in synthesis of reversible and quantum logic, as well as most common misconceptions.
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 introduce a complete transformation rule set and a minimal equation set for controlled-NOT (CNOT)-based quantum circuits. Using these rules, quantum circuits that compute the same Boolean function are reduced to a same normal form. We can thus easily check the equivalence of circuits by comparing their normal forms. By applying the Knuth-Bendix completion algorithm to a set of modified 18 equations introduced by Iwama et al. 2002 [IKY02], we obtain a complete transformation rule set (i.e., a set of transformation rules with the properties of `termination' and `confluence'). Our transformation rule set consists of 114 rules. Moreover, we found a minimal subset of equations for the initial equation set.
We introduce a complete transformation rule set and a minimal equation set for controlled-NOT (CNOT)-based quantum circuits. Using these rules, quantum circuits that compute the same Boolean function are reduced to the same normal form. We can thus easily check the equivalence of circuits by comparing their normal forms. By applying the Knuth-Bendix completion algorithm to a set of modified 18 equations introduced by Iwama et al. 2002, we obtain a complete transformation rule set (i.e., a set of transformation rules with the properties of `termination' and `confluence'). Our transformation rule set consists of 114 rules. Moreover, we discovered a minimal combination of equations for the initial equation set.
Reversible circuits are an emerging technology where all computations are performed in an invertible manner. Motivated by their promising applications, e.g. in the domain of quantum computation or in the low-power design, the synthesis of such circuits has been intensely studied. However, how to automatically realize reversible circuits with the minimal number of lines for large functions is an open research problem. In this paper, we propose a new synthesis approach which relies on concepts that are complementary to existing ones. While “conventional” function representations have been applied for synthesis so far (such as truth tables, ESOPs, BDDs), we exploit Quantum Multiple-valued Decision Diagrams (QMDDs) for this purpose. An algorithm is presented that performs transformations on this data-structure eventually leading to the desired circuit. Experimental results show the novelty of the proposed approach through enabling automatic synthesis of large reversible functions with the minimal number of circuit lines. Furthermore, the quantum cost of the resulting circuits is reduced by 50% on average compared to an existing state-of-the-art synthesis method.