Quantum Graph-State Synthesis with SAT

TL;DR

This paper presents a CNF encoding for both local and non-local graph state operations, corresponding to one- and two-qubit Clifford gates and single-qubit Pauli measurements, and provides an upper bound on the length of the transformation if it exists.

Abstract

In quantum computing and quantum information processing, graph states are a specific type of quantum states which are commonly used in quantum networking and quantum error correction. A recurring problem is finding a transformation from a given source graph state to a desired target graph state using only local operations. Recently it has been shown that deciding transformability is already NP-hard. In this paper, we present a CNF encoding for both local and non-local graph state operations, corresponding to one- and two-qubit Clifford gates and single-qubit Pauli measurements. We use this encoding in a bounded-model-checking set-up to synthesize the desired transformation. Additionally, for a completeness threshold on local transformations, we provide an upper bound on the length of the transformation if it exists. We evaluate the approach in two settings: the first is the synthesis of the ubiquitous GHZ state from a random graph state where we can vary the number of qubits, while the second is based on a proposed 14 node quantum network. We find that the approach is able to synthesize transformations for graphs up to 17 qubits in under 30 minutes.

Figures (5)

• Figure 1: An example 2-qubit quantum circuit. Operations are applied from left to right. The controlled-$Z$ ($\mathit{CZ}$) gate is visualized as . As is common, we write $\ket{01}$ as shorthand for $\ket{0}\otimes\ket{1}$, $\ket{01} = \ket{0}\otimes\ket{1}$, etc. Measuring both qubits at the end gives $\ket{00}$ or $\ket{11}$ with equal probability.
• Figure 2: The circuit in \ref{['fig:example-circuit']} generates the state $\ket{G_2}$, corresponding to the graph in \ref{['fig:example-graph2']}. Examples of local complementation and vertex deletion are shown in \ref{['fig:lc-example']} and \ref{['fig:vd-example']}.
• Figure 3: Graph-state transformation circuit under LC+VD.
• Figure 4: The total SAT solver time for BMC with binary search over the depth up the completeness threshold (see \ref{['sec:max-depth']}). For each number of qubits we run on three Erdős-Rényi random graphs with $p = 0.8$, with a 4-qubit GHZ state as target, with only LC+VD on the left, and LC+VD+EF on a random set $D$ with $|D|=\tfrac{1}{2}|V|$ on the right. \ref{['fig:solv-comp']} shows the difference between the solvers for the data points from both the left and right plot in \ref{['fig:ghz4-time']}. Open symbols indicate timeouts. Solid spheres indicate unreachability at the depth of the completeness threshold. The largest solved instance is for 17 qubits at $d=16$, which has a formula with $\sim$2400 variables and $\sim$300,000 clauses (see above \ref{['eq:R-global']} for $d=1$).
• Figure 5: The 14-node quantum network proposed in rabbie2022designing, and the SAT solver time to synthesize a transformation into a GHZ state for different amounts of entanglement ($p$) in the network. Open circles indicate timeouts. Solid spheres indicate unreachability as at the depth of the completeness threshold.

Theorems & Definitions (3)

• Example 2.1
• Definition 2.1: Graph-state synthesis
• Definition 3.1: Graph encoding