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. For a completeness threshold, 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.

翻译：在量子计算与量子信息处理中，图态是一类特定的量子态，广泛应用于量子网络与量子纠错领域。其中存在一个反复出现的问题：如何仅通过局域操作，将给定的源图态变换为期望的目标图态。近期研究表明，判断可变换性已属NP-hard问题。本文针对图态的局域与非局域操作（分别对应单量子比特与双量子比特的克利福德门，以及单量子比特的泡利测量），提出了相应的CNF编码方案。我们将该编码应用于有界模型检验框架，以合成所需的变换。针对完备性阈值，我们给出了存在变换时其长度的上界。我们在两种场景下评估该方法：其一为从随机图态合成普适的GHZ态（可改变量子比特数量），其二为基于一个拟议的14节点量子网络。实验表明，该方法能在30分钟内完成最多17个量子比特的图态变换合成。