Showing 1–8 of 8 results for author: Amy, M

Optimising T-count is NP-hard

Authors: John van de Wetering, Matt Amy

Abstract: In this short note we show that Boolean satisfiability reduces to finding the optimal number of T gates of a quantum circuit, and hence that optimising T-count is NP-hard. We show that the same argument extends to optimising the number of Toffoli gates in a reversible classical circuit, and we furthermore find an upper bound to the T-count problem of $\text{NP}^{\text{NQP}}$. In this short note we show that Boolean satisfiability reduces to finding the optimal number of T gates of a quantum circuit, and hence that optimising T-count is NP-hard. We show that the same argument extends to optimising the number of Toffoli gates in a reversible classical circuit, and we furthermore find an upper bound to the T-count problem of $\text{NP}^{\text{NQP}}$. △ Less

Submitted 17 October, 2023; v1 submitted 12 September, 2023; originally announced October 2023.

Comments: 3 pages. v2: added proof of hardness of Toffoli optimisation, and improved upper bound of NP^NQP

Improved Synthesis of Toffoli-Hadamard Circuits

Authors: Matthew Amy, Andrew N. Glaudell, Sarah Meng Li, Neil J. Ross

Abstract: The matrices that can be exactly represented by a circuit over the Toffoli-Hadamard gate set are the orthogonal matrices of the form $M/ \sqrt{2}{}^k$, where $M$ is an integer matrix and $k$ is a nonnegative integer. The exact synthesis problem for this gate set is the problem of constructing a circuit for a given such matrix. Existing methods produce circuits consisting of $O(2^n \log(n)k)$ gates… ▽ More The matrices that can be exactly represented by a circuit over the Toffoli-Hadamard gate set are the orthogonal matrices of the form $M/ \sqrt{2}{}^k$, where $M$ is an integer matrix and $k$ is a nonnegative integer. The exact synthesis problem for this gate set is the problem of constructing a circuit for a given such matrix. Existing methods produce circuits consisting of $O(2^n \log(n)k)$ gates, where $n$ is the dimension of the matrix. In this paper, we provide two improved synthesis methods. First, we show that a technique introduced by Kliuchnikov in 2013 for Clifford+$T$ circuits can be straightforwardly adapted to Toffoli-Hadamard circuits, reducing the complexity of the synthesized circuit from $O(2^n \log(n)k)$ to $O(n^2 \log(n)k)$. Then, we present an alternative synthesis method of similarly improved cost, but whose application is restricted to circuits on no more than three qubits. Our results also apply to orthogonal matrices over the dyadic fractions, which correspond to circuits using the 2-qubit gate $H\otimes H$, rather than the usual single-qubit Hadamard gate $H$. △ Less

Submitted 18 May, 2023; originally announced May 2023.

Sized Types for low-level Quantum Metaprogramming

Authors: Matthew Amy

Abstract: One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, an ability which is of particular importance in the context of quantum computing as algorithms frequently use arithmetic over non-standard word l… ▽ More One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, an ability which is of particular importance in the context of quantum computing as algorithms frequently use arithmetic over non-standard word lengths. In this work, we introduce metaQASM, a typed extension of the openQASM language supporting the metaprogramming of circuit families. Our language and type system, built around a lightweight implementation of sized types, supports subty** over register sizes and is moreover type-safe. In particular, we prove that our system is strongly normalizing, and as such any well-typed metaQASM program can be statically unrolled into a finite circuit. △ Less

Submitted 7 August, 2019; originally announced August 2019.

Comments: Presented at Reversible Computation 2019. Final authenticated publication is available online at https://doi.org/10.1007/978-3-030-21500-2_6

Journal ref: Thomsen M., Soeken M. (eds) Reversible Computation. RC 2019. Lecture Notes in Computer Science, vol 11497. Springer, Cham

Towards Large-scale Functional Verification of Universal Quantum Circuits

Authors: Matthew Amy

Abstract: We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy… ▽ More We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy with respect to either a specification or reference circuit is enabled by a novel rewrite system for exponential sums with free variables. Our algorithm is further shown to give a polynomial-time decision procedure for checking the equivalence of Clifford group circuits. We evaluate our methods by performing automated verification of optimized Clifford+T circuits with up to 100 qubits and thousands of T gates, as well as the functional verification of quantum algorithms using hundreds of qubits. Our experiments culminate in the automated verification of the Hidden Shift algorithm for a class of Boolean functions in a fraction of the time it has taken recent algorithms to simulate. △ Less

Submitted 29 January, 2019; v1 submitted 17 May, 2018; originally announced May 2018.

Comments: In Proceedings QPL 2018, arXiv:1901.09476

Journal ref: EPTCS 287, 2019, pp. 1-21

A Finite Presentation of CNOT-Dihedral Operators

Authors: Matthew Amy, Jianxin Chen, Neil J. Ross

Abstract: We give a finite presentation by generators and relations of the unitary operators expressible over the {CNOT, T, X} gate set, also known as CNOT-dihedral operators. To this end, we introduce a notion of normal form for CNOT-dihedral circuits and prove that every CNOT-dihedral operator admits a unique normal form. Moreover, we show that in the presence of certain structural rules only finitely man… ▽ More We give a finite presentation by generators and relations of the unitary operators expressible over the {CNOT, T, X} gate set, also known as CNOT-dihedral operators. To this end, we introduce a notion of normal form for CNOT-dihedral circuits and prove that every CNOT-dihedral operator admits a unique normal form. Moreover, we show that in the presence of certain structural rules only finitely many circuit identities are required to reduce an arbitrary CNOT-dihedral circuit to its normal form. By appropriately restricting our relations, we obtain a finite presentation of unitary operators expressible over the {CNOT, T} gate set as a corollary. △ Less

Submitted 28 April, 2019; v1 submitted 31 December, 2016; originally announced January 2017.

Comments: In Proceedings QPL 2017, arXiv:1802.09737

Journal ref: EPTCS 266, 2018, pp. 84-97

Verified compilation of space-efficient reversible circuits

Authors: Matthew Amy, Martin Roetteler, Krysta Svore

Abstract: The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent on… ▽ More The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent on verifying the correctness of the results, an issue of particular importance in quantum computing. There, compilation allows not only map** to hardware, but also the estimation of resources required to implement a given quantum algorithm, a process that is crucial for identifying which algorithms will outperform their classical counterparts. We present a reversible circuit compiler called ReVerC, which has been formally verified in F* and compiles circuits that operate correctly with respect to the input program. Our compiler compiles the Revs language to combinational reversible circuits with as few ancillary bits as possible, and provably cleans temporary values. △ Less

Submitted 20 April, 2018; v1 submitted 4 March, 2016; originally announced March 2016.

Comments: Proceedings version. New section on eager cleanup, general streamlining

Journal ref: Proceedings of the 29th International Conference on Computer Aided Verification, pp. 3-21, 2017

Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning

Authors: Matthew Amy, Dmitri Maslov, Michele Mosca

Abstract: Most work in quantum circuit optimization has been performed in isolation from the results of quantum fault-tolerance. Here we present a polynomial-time algorithm for optimizing quantum circuits that takes the actual implementation of fault-tolerant logical gates into consideration. Our algorithm re-synthesizes quantum circuits composed of Clifford group and T gates, the latter being typically the… ▽ More Most work in quantum circuit optimization has been performed in isolation from the results of quantum fault-tolerance. Here we present a polynomial-time algorithm for optimizing quantum circuits that takes the actual implementation of fault-tolerant logical gates into consideration. Our algorithm re-synthesizes quantum circuits composed of Clifford group and T gates, the latter being typically the most costly gate in fault-tolerant models, e.g., those based on the Steane or surface codes, with the purpose of minimizing both T-count and T-depth. A major feature of the algorithm is the ability to re-synthesize circuits with additional ancillae to reduce T-depth at effectively no cost. The tested benchmarks show up to 65.7% reduction in T-count and up to 87.6% reduction in T-depth without ancillae, or 99.7% reduction in T-depth using ancillae. △ Less

Submitted 13 December, 2013; v1 submitted 8 March, 2013; originally announced March 2013.

Comments: Version 2 contains substantial improvements and extensions to the previous version. We describe a new, more robust algorithm and achieve significantly improved experimental results

Journal ref: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 33(10): 1476-1489, 2014

A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits

Authors: Matthew Amy, Dmitri Maslov, Michele Mosca, Martin Roetteler

Abstract: We present an algorithm for computing depth-optimal decompositions of logical operations, leveraging a meet-in-the-middle technique to provide a significant speed-up over simple brute force algorithms. As an illustration of our method we implemented this algorithm and found factorizations of the commonly used quantum logical operations into elementary gates in the Clifford+T set. In particular, we… ▽ More We present an algorithm for computing depth-optimal decompositions of logical operations, leveraging a meet-in-the-middle technique to provide a significant speed-up over simple brute force algorithms. As an illustration of our method we implemented this algorithm and found factorizations of the commonly used quantum logical operations into elementary gates in the Clifford+T set. In particular, we report a decomposition of the Toffoli gate over the set of Clifford and T gates. Our decomposition achieves a total T-depth of 3, thereby providing a 40% reduction over the previously best known decomposition for the Toffoli gate. Due to the size of the search space the algorithm is only practical for small parameters, such as the number of qubits, and the number of gates in an optimal implementation. △ Less

Submitted 25 January, 2013; v1 submitted 4 June, 2012; originally announced June 2012.

Comments: 23 pages, 15 figures, 1 table; To appear in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

Journal ref: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 32(6): 818-830, 2013