Quantum Graph-State Synthesis with SAT

TL;DR

This paper introduces a SAT-based method for synthesizing quantum graph states, enabling the transformation from source to target states efficiently, with practical evaluation on states up to 17 qubits.

Contribution

It presents a novel CNF encoding for quantum graph state transformations and applies bounded-model-checking to synthesize desired states.

Findings

Successfully synthesizes transformations for up to 17 qubits

Efficiently handles both local and non-local operations

Provides bounds on transformation lengths

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.