Distributing Quantum Circuits Using Formal Methods.

This paper presents a vision for generating formal specifications of the problems involved in the mapping of quantum algorithms to quantum networks, called the Sub-problems of Distribution (SpD). This is a significant challenge due to the importance of distributed quantum computing and the intertwined nature of SpD. Examples of SpD include teleportation minimization, qubit routing and load balancing. As such, formal specifications can help in providing a rigorous way for specifying and solving SpD. We instantiate the proposed vision in the context of Alloy, called qcAlloy, and for two of the most important SpD problems, namely teleportation minimization and load balancing. Part of the Alloy specifications that specify the constraints of SpD are reusable for any quantum circuit and any network. qcAlloy is also compositional in that it partitions the input circuit into sub-circuits, solves the SpD for each sub-circuit, and then combines the results towards generating a nearoptimal solution. qcAlloy competes, and in some cases outperforms, the state-of-the-art for minimizing the number of teleportations for the quantum circuits in the RevLib and RLSB benchmarks.