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

International Symposium on Advances in Electrical, Electronics and Computer Engineering (ISAEECE)

Synthesizing reversible functions via bounded model checking

Xiao Zeng, Jinzhao Wu, Guowu Yang

Published May 31, 2023• 0 citations
Publisher

Abstract

We consider the problem of synthesizing optimized circuits for reversible functions using NOT, CNOT and Toffoli gates (NCT), which has important applications in circuit design and quantum cryptography. By defining the state space and state transitions from NCT gates, we transform the synthesis problem into a reachability problem of finding the shortest path connecting the identity function and the targeted function that is to be synthesized. Using Bounded Model Checking (BMC), we propose an algorithm for synthesizing the optimized circuit for reversible functions. For the synthesis of linear reversible functions, we design another method by directly parametrizing the linear invertible matrix. Our methods can produce optimal synthesis of reversible circuits when the number of bits is small, and also can be used as a subroutine of heuristic methods for large bits. Experimental results show the effectiveness of our methods.

DOI
10.1117/12.2680559

Related papers

Optimization of Reversible Circuits Using Toffoli Decompositions with Negative Controls

Mariam Gado, Ahmed Younes

The synthesis and optimization of quantum circuits are essential for the construction of quantum computers. This paper proposes two methods to reduce the quantum cost of 3-bit reversible circuits. The first method utilizes basic building blocks of gate pairs using different Toffoli decompositions. These gate pairs are used to reconstruct the quantum circuits where further optimization rules will be applied to synthesize the optimized circuit. The second method suggests using a new universal library, which provides better quantum cost when compared with previous work in both cost015 and cost115 metrics; this proposed new universal library “Negative NCT” uses gates that operate on the target qubit only when the control qubit’s state is zero. A combination of the proposed basic building blocks of pairs of gates and the proposed Negative NCT library is used in this work for synthesis and optimization, where the Negative NCT library showed better quantum cost after optimization compared with the NCT library despite having the same circuit size. The reversible circuits over three bits form a permutation group of size 40,320 (23!), which is a subset of the symmetric group, where the NCT library is considered as the generators of the permutation group.

Symmetry•Jun 7, 2021•8 citations

Systematic Synthesis and Optimization of Reversible Quantum Circuits via MINLP, Toffoli Permutation, and Local Search

GEORGE PAPAKONSTANTINOU

The synthesis of efficient reversible logic circuits is critical for fault-tolerant quantum computing (FTQC). The primary motivation of this work is to overcome the inherent disadvantages of existing synthesis techniques: approximate heuristic methods often miss optimal solutions, while pure exact computational methods suffer from combinatorial explosion on deep circuits. While the strict NCT library (NOT, CNOT, Toffoli) is often preferred due to the high cost of distilling non-Clifford states required for arbitrary gates, standard physical implementations frequently utilize the broader NCV library (NOT, CNOT, V, V-dagger), requiring the decomposition of Toffoli gates into five elementary operations. To bridge this gap, this paper presents a unified, highly scalable methodology for the optimal design of reversible circuits across both libraries. First, a Mixed-Integer Non-Linear Programming (MINLP) formulation, linearized for the high-performance IBM ILOG CPLEX solver, is introduced to automate the exact generation of globally optimal strict NCT topologies. Second, a systematic four-phase optimization framework is proposed to reduce NCV costs. By replacing Toffoli gates with specific NCV decompositions, permuting control lines to match subsequent linear gates, and applying exact local searches via an extended MINLP solver on bounded sliding windows, significant gate cancellations are achieved. Applying this methodology to prominent primitives (MIG, SAYEM, URG, TSG, and MKG), we match global NCT optimality constraints and achieve highly optimized NCV Quantum Costs of 7, 14, and 12 for the MIG, TSG, and MKG gates, respectively, establishing best-known upper bounds that significantly outperform heuristic literature benchmarks.

Quantum Reports•Aug 14, 2026•0 citations

Optimal and asymptotically optimal NCT reversible circuits by the gate types

Dmitri Maslov

We report optimal and asymptotically optimal reversible circuits composed of NOT, CNOT, and Toffoli (NCT) gates, keeping the count by the subsets of the gate types used. This study fine tunes the circuit complexity figures for the realization of reversible functions via reversible NCT circuits. An important consequence is a result on the limitation of the use of the T-count quantum circuit metric popular in applications.

Quantum Information and Computation•Oct 1, 2016•20 citations

A Novel Efficient Optimal Reversible Circuit Synthesis Algorithm

Yu-Shan Yang, Han-Kuan Chen, Shu–Yu Kuo +2 more

In quantum computing, the synthesis of reversible circuits is an important topic. Reversible circuit synthesis is particularly challenging because the complexity grows as the number of bits increases. To date, many reversible circuit synthesis algorithms have been proposed, but most are unable to find the optima within an acceptable time. Because traditional methods only consider partial interests, the resulting cost would be more gates. This paper proposes a novel method, called Bound Oriented Algorithm, which has the ability to find the optimal solution with a high hit rate, one greater than 75% on average. Moreover, with the prediction of the optima by bound, it can reduce excess calculation to further improve efficiency. In addition, a special library containing only Toffoli gates is used, which simplifies algorithm design and is more easily converted to a common library. The experiment result shows that the proposed method performs better than other methods in terms of solution quality and time cost.

Conference proceedings/Conference proceedings - IEEE International Conference on Systems, Man, and Cybernetics•Oct 1, 2015•2 citations

An Algorithm for Reversible Logic Circuit Synthesis Based on Tensor Decomposition

Hochang Lee, Kyung Chul Jeong, Daewan Han +1 more

An algorithm for reversible logic synthesis is proposed. The task is, for a given n -bit substitution map, to find a sequence of reversible logic gates that implements the map. The gate library adopted in this work consists of multiple-controlled Toffoli gates with m control bits, where \(m \in \lbrace 0, \ldots , n-1\rbrace\) . Controlled gates with large m (> 2) are then further decomposed into smaller gates ( \(m \le 2\) ). A primary goal in designing the algorithm is to reduce the number of Toffoli gates, which is known to be universal. The main idea is to view an n -bit substitution map as a rank-2 n tensor and to transform it such that the resulting map can be written as a tensor product of a rank-(2 n -2) tensor and the 2× 2 identity matrix. It can then be seen that the transformed map acts nontrivially on n -1 bits only, meaning that the map to be synthesized becomes ( n -1)-bit substitution. This size reduction process is iteratively applied until it reaches a tensor product of only 2× 2 matrices. The time complexity of the algorithm is exponential in n , as most previously known heuristic algorithms for reversible logic synthesis are, but it terminates within reasonable time for not too large n , which may find practical uses. As stated earlier, our primary target is to reduce the number of Toffoli gates in the output circuit. Benchmark results show that the algorithm works well for hard benchmark functions, but it does not seem advantageous when the function is structured. As an application, the algorithm is applied to find reversible circuits for cryptographic substitution boxes, which are often required in quantum cryptanalysis.

arXiv:2107.04298•ACM Transactions on Quantum Computing•Jun 18, 2024•5 citations

A Novel Algorithm for Reversible Circuit Optimization

Yi-Tzu Lo, Shu–Yu Kuo, Guo-Jyun Zeng +2 more

Reversible circuit synthesis is an important field in quantum computing, low-power design, and reversible circuit. The problem of reversible circuit synthesis is complicated and hard to solve because the input of the reversible circuit will experience a huge increase when extended to multi-bit. In this paper, a novel algorithm of reversible circuit synthesis is proposed. With the satisfied priority of positions, we can efficiently select the position which should be satisfied, and each selected gate is generated to benefit the overall situation. Therefore, the proposed algorithm is able to optimize the reversible circuit with fewer gates and can be implemented in regard to multibit reversible circuit synthesis. In addition, the gate set we used contains only Toffoli, spanning all wires. This Toffoli gate is liable to be transformed into another gate set and is helpful for algorithm design. The experiment shows that the proposed algorithm, with efficient and optimal results, is superior to others.

Conference proceedings/Conference proceedings - IEEE International Conference on Systems, Man, and Cybernetics•Oct 1, 2015•1 citation
We consider the problem of synthesizing optimized circuits for reversible functions using NOT, CNOT and Toffoli gates (NCT), which has important applications in circuit design and quantum cryptography. By defining the state space and state transitions from NCT gates, we transform the synthesis problem into a reachability problem of finding the shortest path connecting the identity function and the targeted function that is to be synthesized. Using Bounded Model Checking (BMC), we propose an algorithm for synthesizing the optimized circuit for reversible functions. For the synthesis of linear reversible functions, we design another method by directly parametrizing the linear invertible matrix. Our methods can produce optimal synthesis of reversible circuits when the number of bits is small, and also can be used as a subroutine of heuristic methods for large bits. Experimental results show the effectiveness of our methods.
The synthesis and optimization of quantum circuits are essential for the construction of quantum computers. This paper proposes two methods to reduce the quantum cost of 3-bit reversible circuits. The first method utilizes basic building blocks of gate pairs using different Toffoli decompositions. These gate pairs are used to reconstruct the quantum circuits where further optimization rules will be applied to synthesize the optimized circuit. The second method suggests using a new universal library, which provides better quantum cost when compared with previous work in both cost015 and cost115 metrics; this proposed new universal library “Negative NCT” uses gates that operate on the target qubit only when the control qubit’s state is zero. A combination of the proposed basic building blocks of pairs of gates and the proposed Negative NCT library is used in this work for synthesis and optimization, where the Negative NCT library showed better quantum cost after optimization compared with the NCT library despite having the same circuit size. The reversible circuits over three bits form a permutation group of size 40,320 (23!), which is a subset of the symmetric group, where the NCT library is considered as the generators of the permutation group.
The synthesis of efficient reversible logic circuits is critical for fault-tolerant quantum computing (FTQC). The primary motivation of this work is to overcome the inherent disadvantages of existing synthesis techniques: approximate heuristic methods often miss optimal solutions, while pure exact computational methods suffer from combinatorial explosion on deep circuits. While the strict NCT library (NOT, CNOT, Toffoli) is often preferred due to the high cost of distilling non-Clifford states required for arbitrary gates, standard physical implementations frequently utilize the broader NCV library (NOT, CNOT, V, V-dagger), requiring the decomposition of Toffoli gates into five elementary operations. To bridge this gap, this paper presents a unified, highly scalable methodology for the optimal design of reversible circuits across both libraries. First, a Mixed-Integer Non-Linear Programming (MINLP) formulation, linearized for the high-performance IBM ILOG CPLEX solver, is introduced to automate the exact generation of globally optimal strict NCT topologies. Second, a systematic four-phase optimization framework is proposed to reduce NCV costs. By replacing Toffoli gates with specific NCV decompositions, permuting control lines to match subsequent linear gates, and applying exact local searches via an extended MINLP solver on bounded sliding windows, significant gate cancellations are achieved. Applying this methodology to prominent primitives (MIG, SAYEM, URG, TSG, and MKG), we match global NCT optimality constraints and achieve highly optimized NCV Quantum Costs of 7, 14, and 12 for the MIG, TSG, and MKG gates, respectively, establishing best-known upper bounds that significantly outperform heuristic literature benchmarks.
In quantum computing, the synthesis of reversible circuits is an important topic. Reversible circuit synthesis is particularly challenging because the complexity grows as the number of bits increases. To date, many reversible circuit synthesis algorithms have been proposed, but most are unable to find the optima within an acceptable time. Because traditional methods only consider partial interests, the resulting cost would be more gates. This paper proposes a novel method, called Bound Oriented Algorithm, which has the ability to find the optimal solution with a high hit rate, one greater than 75% on average. Moreover, with the prediction of the optima by bound, it can reduce excess calculation to further improve efficiency. In addition, a special library containing only Toffoli gates is used, which simplifies algorithm design and is more easily converted to a common library. The experiment result shows that the proposed method performs better than other methods in terms of solution quality and time cost.
An algorithm for reversible logic synthesis is proposed. The task is, for a given n -bit substitution map, to find a sequence of reversible logic gates that implements the map. The gate library adopted in this work consists of multiple-controlled Toffoli gates with m control bits, where m∈{0,…,n−1}m \in \lbrace 0, \ldots , n-1\rbracem∈{0,…,n−1} . Controlled gates with large m (> 2) are then further decomposed into smaller gates ( m≤2m \le 2m≤2 ). A primary goal in designing the algorithm is to reduce the number of Toffoli gates, which is known to be universal. The main idea is to view an n -bit substitution map as a rank-2 n tensor and to transform it such that the resulting map can be written as a tensor product of a rank-(2 n -2) tensor and the 2× 2 identity matrix. It can then be seen that the transformed map acts nontrivially on n -1 bits only, meaning that the map to be synthesized becomes ( n -1)-bit substitution. This size reduction process is iteratively applied until it reaches a tensor product of only 2× 2 matrices. The time complexity of the algorithm is exponential in n , as most previously known heuristic algorithms for reversible logic synthesis are, but it terminates within reasonable time for not too large n , which may find practical uses. As stated earlier, our primary target is to reduce the number of Toffoli gates in the output circuit. Benchmark results show that the algorithm works well for hard benchmark functions, but it does not seem advantageous when the function is structured. As an application, the algorithm is applied to find reversible circuits for cryptographic substitution boxes, which are often required in quantum cryptanalysis.
Reversible circuit synthesis is an important field in quantum computing, low-power design, and reversible circuit. The problem of reversible circuit synthesis is complicated and hard to solve because the input of the reversible circuit will experience a huge increase when extended to multi-bit. In this paper, a novel algorithm of reversible circuit synthesis is proposed. With the satisfied priority of positions, we can efficiently select the position which should be satisfied, and each selected gate is generated to benefit the overall situation. Therefore, the proposed algorithm is able to optimize the reversible circuit with fewer gates and can be implemented in regard to multibit reversible circuit synthesis. In addition, the gate set we used contains only Toffoli, spanning all wires. This Toffoli gate is liable to be transformed into another gate set and is helpful for algorithm design. The experiment shows that the proposed algorithm, with efficient and optimal results, is superior to others.