Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond

• URL: http://arxiv.org/abs/2203.00698v1
• Date: Tue, 1 Mar 2022 19:00:02 GMT
• Title: Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond
• Authors: Lucas Berent, Lukas Burgholzer, Robert Wille
• Abstract summary: We propose a propositional SAT encoding that can be applied to arbitrary quantum circuits. We show that due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative.
• Score: 3.610459670994051
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Satisfiability Testing (SAT) techniques are well-established in classical computing where they are used to solve a broad variety of problems, e.g., in the design of classical circuits and systems. Analogous to the classical realm, quantum algorithms are usually modelled as circuits and similar design tasks need to be tackled. Thus, it is natural to pose the question whether these design tasks in the quantum realm can also be approached using SAT techniques. To the best of our knowledge, no SAT formulation for arbitrary quantum circuits exists and it is unknown whether such an approach is feasible at all. In this work, we define a propositional SAT encoding that, in principle, can be applied to arbitrary quantum circuits. However, we show that due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. Therefore, we establish general criteria for determining the feasibility of the proposed encoding and identify classes of quantum circuits fulfilling these criteria. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative. Finally, we empirically demonstrate the applicability and efficiency of the proposed encoding for Clifford circuits. With these results, we lay the foundation for continuing the ongoing success of SAT in classical circuit and systems design for quantum circuits.

Related papers

• Clifford and Non-Clifford Splitting in Quantum Circuits: Applications and ZX-Calculus Detection Procedure [49.1574468325115]
  We propose and analyze use cases that come from quantum circuits that can be written as product between a Clifford and a Non-Clifford unitary. We make use of ZX-Calculus and its assets to detect a limiting border of these circuits that would allow for a separation between a Clifford section and a Non-Clifford section.
  arXiv  Detail & Related papers  (2025-04-22T16:10:34Z)
• Data Complexity Measures for Quantum Circuits Architecture Recommendation [55.74527632797241]
  Quantum Parametric Circuits are constructed as an alternative to reduce the size of quantum circuits. determining the optimal circuit for a given problem remains an open question. In this work, a quantum circuit recommendation architecture for classification problems is proposed using database complexity measures.
  arXiv  Detail & Related papers  (2025-02-21T01:17:24Z)
• Redesign Quantum Circuits on Quantum Hardware Device [6.627541720714792]
  We present a new architecture which enables one to redesign large-scale quantum circuits on quantum hardware. For concreteness, we apply this architecture to three crucial applications in circuit optimization, including the equivalence checking of (non-) parameterized circuits. The feasibility of our approach is demonstrated by the excellent results of these applications, which are implemented both in classical computers and current NISQ hardware.
  arXiv  Detail & Related papers  (2024-12-30T12:05:09Z)
• Simulating Quantum Circuits by Model Counting [0.0]
  We show for the first time that a strong simulation of universal quantum circuits can be efficiently tackled through weighted model counting. Our work paves the way to apply the existing array of powerful classical reasoning tools to realize efficient quantum circuit compilation.
  arXiv  Detail & Related papers  (2024-03-11T22:40:15Z)
• Quantum circuit debugging and sensitivity analysis via local inversions [62.997667081978825]
  We present a technique that pinpoints the sections of a quantum circuit that affect the circuit output the most. We demonstrate the practicality and efficacy of the proposed technique by applying it to example algorithmic circuits implemented on IBM quantum machines.
  arXiv  Detail & Related papers  (2022-04-12T19:39:31Z)
• Gaussian initializations help deep variational quantum circuits escape from the barren plateau [87.04438831673063]
  Variational quantum circuits have been widely employed in quantum simulation and quantum machine learning in recent years. However, quantum circuits with random structures have poor trainability due to the exponentially vanishing gradient with respect to the circuit depth and the qubit number. This result leads to a general belief that deep quantum circuits will not be feasible for practical tasks.
  arXiv  Detail & Related papers  (2022-03-17T15:06:40Z)
• An Optimized Quantum Implementation of ISD on Scalable Quantum Resources [2.274915755738124]
  We show that Prange's ISD algorithm can be implemented rather efficiently on a quantum computer. We leverage the idea of classical co-processors to design hybrid classical-quantum trade-offs.
  arXiv  Detail & Related papers  (2021-12-12T06:01:10Z)
• Gottesman Types for Quantum Programs [0.0]
  We show that Gottesman's semantics for quantum programs can be treated as a type system. We also show that it can be extended beyond the Clifford set to partially characterize a broad range of programs.
  arXiv  Detail & Related papers  (2021-09-06T01:02:01Z)
• Handling Non-Unitaries in Quantum Circuit Equivalence Checking [4.265279817927261]
  Quantum computers are reaching a level where interactions between classical and quantum computations can happen in real-time. This marks the advent of a new, broader class of quantum circuits: dynamic quantum circuits. They offer a broader range of available computing primitives that lead to new challenges for design tasks such as simulation, compilation, and verification.
  arXiv  Detail & Related papers  (2021-06-02T12:04:56Z)
• Error mitigation and quantum-assisted simulation in the error corrected regime [77.34726150561087]
  A standard approach to quantum computing is based on the idea of promoting a classically simulable and fault-tolerant set of operations. We show how the addition of noisy magic resources allows one to boost classical quasiprobability simulations of a quantum circuit.
  arXiv  Detail & Related papers  (2021-03-12T20:58:41Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)
• Efficient simulatability of continuous-variable circuits with large Wigner negativity [62.997667081978825]
  Wigner negativity is known to be a necessary resource for computational advantage in several quantum-computing architectures. We identify vast families of circuits that display large, possibly unbounded, Wigner negativity, and yet are classically efficiently simulatable. We derive our results by establishing a link between the simulatability of high-dimensional discrete-variable quantum circuits and bosonic codes.
  arXiv  Detail & Related papers  (2020-05-25T11:03:42Z)
• Classical Coding Approaches to Quantum Applications [2.5382095320488665]
  In deep-space optical communications, current receivers for the pure-state-quantum channel first measure each qubit channel output and then classically post-process the measurements. In this dissertation we investigate a recently proposed quantum algorithm for this task, which is inspired by classical belief-propagation algorithms. We show that the algorithm is optimal for each bit and it appears to achieve optimal performance when deciding the full transmitted message.
  arXiv  Detail & Related papers  (2020-04-14T23:31:46Z)
• Hardware-Encoding Grid States in a Non-Reciprocal Superconducting Circuit [62.997667081978825]
  We present a circuit design composed of a non-reciprocal device and Josephson junctions whose ground space is doubly degenerate and the ground states are approximate codewords of the Gottesman-Kitaev-Preskill (GKP) code. We find that the circuit is naturally protected against the common noise channels in superconducting circuits, such as charge and flux noise, implying that it can be used for passive quantum error correction.
  arXiv  Detail & Related papers  (2020-02-18T16:45:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.