# Synthesis of Clifford Circuits#

Executing quantum circuits on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device. Due to device’s limited coherence times and gate fidelity, the compilation process has to be optimized as much as possible. To this end, an algorithm’s description first has to be *synthesized* using the device’s gate library. In addition, circuits have to be *mapped* to the target quantum device to satisfy its connectivity constraints. Even though
Clifford circuits form a finite subgroup of all quantum circuits – one that is not even universal for quantum computing – the search space for these problems grows exponentially with respect to the number of considered qubits.

The *Clifford synthesis approach* in QMAP can be used to produce optimal Clifford circuits based on the methods proposed in [7]. To this end, it encodes the underlying task as a satisfiability (SAT) problem and solves it using the SMT solver Z3 in conjunction with a binary search scheme.

The following gives a brief overview on Clifford circuits and how QMAP can be used for their synthesis.

## Clifford Circuits#

Clifford circuits, i.e., circuits generated from the set \(\{H, S, \mathit{CNOT}\}\), form an important subclass of quantum circuits. This is due to several factors

According to the Gottesman-Knill theorem, they can be simulated in polynomial time and space on classical computers using the

*stabilizer*formalism.They can be used to describe several quantum phenomena such as superposition, entanglement, superdense coding, and teleportation.

Many error correcting codes rely on them.

Quantum states that can be obtained from the all-zero basis state \(|0\dots 0\rangle\) by applying Clifford operations are called stabilizer states. The name originates from the fact that such a state is uniquely and efficiently described by the set of operators that generate the group of its stabilizers. Specifically, any *n*-qubit stabilizer state can be described by a set of *n* Pauli strings \(\pm P_{i,0}P_{i,1}P_{i,2}\dots P_{i,n-1}\), with \(P_{i,j}\in\{I, X, Y, Z\}\) and
\(i, j\in 0,\dots, n-1\). Hence,two bits per qubit are needed to identify the Pauli operator, as well as one additional bit for the phase, which leads to a total of $n(2n+1)` bits needed to uniquely describe a particular stabilizer state.

The stabilizer representation of a quantum state is conveniently described by a *tableau*:

Here, the binary variables \(x_{ij}\) and \(z_{ij}\) specify whether the Pauli term \(P_{i,j}\) is \(X\) or \(Z\), respectively. Since \(Y = iXZ\), setting \(x_{ij} = z_{ij} = 1\) corresponds to \(P_{i,j}=Y\). Finally, \(r_i\) describes whether the generator has a negative phase.

Consider the following quantum circuit:

```
[1]:
```

```
from qiskit import QuantumCircuit
qc = QuantumCircuit(2)
qc.h(0)
qc.cx(0, 1)
qc.h(0)
qc.h(1)
qc.draw(output="mpl")
```

```
[1]:
```

Then, the corresponding stabilizer tableau is

```
0 0 | 1 1 | 0
1 1 | 0 0 | 0
```

which corresponds to the stabilizers

```
[2]:
```

```
stabilizers = ["+ZZ", "+XX"]
```

The stabilizer tableau does not fix a unitary operator uniquely. As stated above, the stabilizers only fix the state that is obtained by applying a unitary to the all-zero basis state. The following circuit also produces the same state as the one above:

```
[3]:
```

```
from qiskit import QuantumCircuit
qc_alt = QuantumCircuit(2)
qc_alt.z(0)
qc_alt.h(0)
qc_alt.cx(0, 1)
qc_alt.h(0)
qc_alt.h(1)
qc_alt.draw(output="mpl")
```

```
[3]:
```

But the first circuit has the unitary

whereas the second circuit has the unitary

To fix the unitary one needs to also take the *destabilizers* into account. The destabilizers are also Pauli strings that together with the stabilizers generate the entire Pauli group.

The destabilizers of the first circuit are

```
[4]:
```

```
destabilizers = ["+IX", "+ZI"]
```

The destabilizers of the second circuit are

```
[5]:
```

```
destabilizers_alt = ["-IX", "+ZI"]
```

## Using QMAP for Optimal Synthesis#

*QMAP* can be used in a multitude of ways to efficiently synthesize Clifford circuits:

### Starting from an initial circuit `qc`

#

```
[6]:
```

```
from qiskit import QuantumCircuit
from mqt import qmap
qc = QuantumCircuit(2)
qc.h(0)
qc.cx(0, 1)
qc.h(0)
qc.h(1)
qc_opt, results = qmap.optimize_clifford(circuit=qc, use_maxsat=True, include_destabilizers=True)
qc_opt.draw(output="mpl")
```

```
[6]:
```

The `include_destabilizers`

flag guarantees that the unitary of the circuit is preserved during optimization.

By default *QMAP* generates optimal Clifford circuits with respect to the target metric. This might lead to runtime problems when trying to optimize larger circuits. When optimizing for depth, *QMAP* provides a heuristic that splits the circuits into several independent parts and optimizes them separately. This allows to optimize larger circuits while not guaranteeing that the depth-optimal circuit is synthesized.

The heuristic synthesizer can be used as follows:

```
[7]:
```

```
from qiskit import QuantumCircuit
from mqt import qmap
qc = QuantumCircuit(2)
qc.x(0)
qc.cx(0, 1)
qc.x(0)
qc.s(1)
qc.x(1)
qc.cx(1, 0)
qc.x(1)
qc_opt, results = qmap.optimize_clifford(
circuit=qc, heuristic=True, split_size=3, include_destabilizers=True, target_metric="depth"
)
qc_opt.draw(output="mpl")
```

```
[7]:
```

The parameter `split_size`

determines how many layers of the circuit are optimized individually.

In this example the synthesized circuit does not have optimal depth as can be checked by running the optimal synthesis method:

```
[8]:
```

```
from qiskit import QuantumCircuit
from mqt import qmap
qc = QuantumCircuit(2)
qc.x(0)
qc.cx(0, 1)
qc.x(0)
qc.s(1)
qc.x(1)
qc.cx(1, 0)
qc.x(1)
qc_opt, results = qmap.optimize_clifford(circuit=qc, heuristic=False, include_destabilizers=True, target_metric="depth")
qc_opt.draw(output="mpl")
```

```
[8]:
```

However, the heuristic still gives a good depth reduction in many cases.

### Starting from a functional description#

```
[9]:
```

```
from mqt import qmap
tableau = qmap.Tableau("['+ZZ', '+XX']")
qc_synth, results = qmap.synthesize_clifford(tableau)
qc_synth.draw(output="mpl")
```

```
[9]:
```

The synthesis method offers lots of configuration options to fine-tune the synthesis procedure, e.g., changing the target metric.

Check out the reference documentation for more information.