Quantum Graph-State Synthesis with SAT

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 Cliford 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.

Keywords

• eol>Quantum computing
• graph states
• bounded model checking

1. Introduction

The creation, manipulation and transmission of quantum information brings into reach applications which are unfeasible or even impossible using classical computers, such as provably-secure communication [ 1, 2 ], more accurate clock synchronization [ 3 ], and chemistry applications [ 4 ]. Various questions regarding simulation, modeling and design of quantum computers and networks can be phrased using graph states, a subset of all possible states of a register of quantum bits (qubits) which can be described using graphs [ 5 ]. Additionally, graph states are crucial to a universal model of quantum computation called measurement-based quantum computing [ 6 ]. Furthermore, when augmented with a finite set of quantum operations called Cliford gates and single-qubit Pauli measurements, the graph-state formalism gives rise to eficient classical simulation of a large class of quantum circuits [ 7 ] and forms the basis for many quantum error correction schemes [ 8 ], a prerequisite for scaling up quantum computing with imperfect devices, as well as many quantum-networking applications [ 9, 5 ]. These applications have a focus on local quantum operations, i.e. on a single or few spatially-close qubits, for reasons regarding experimental implementation with imperfect devices.

Given this wide applicability, graph-state transformations have been extensively studied from the theory standpoint for various sets of allowed local quantum operations [ 10, 11, 12, 13, 5, 14 ]. In this work, we specifically consider the following problem: given a source graph state, synthesize a desired target graph state using single-qubit Cliford gates and single-qubit Pauli measurement. This problem was shown before [ 15 ] to be equivalent to transforming the associated graphs under two graph operations: an edge-toggling operation called local complementation (LC), corresponding to single-qubit Clifords, and vertex deletion (VD), corresponding to measurements. The decision problem (can a source graph be transformed to a target graph under LC+VD?) has been shown to be NP-complete [ 16 ], even when restricting the target graph to a practically-relevant scenario [ 17 ]. Although there exists an algorithm [ 15 ] (based on techniques from [ 18, 19 ]) which is fixed-parameter tractable (FPT) in the rank-width of the graph, the authors of the algorithm themselves remark it is not useful in practice due to a giant FPT-prefactor equalling ten times repeated exponentiation with base 2 (i.e. 22...2 ) [ 16 ].

We tackle the problem of graph-state synthesis under LC+VD with bounded model checking (BMC) [ 20, 21 ]. To this end we present a Boolean encoding for graph states and the operations on them, and provide a completeness threshold for this problem. We also give an encoding for twoqubit graph operations, which together with single-qubit operations enable all possible Cliford operations [ 14 ]. This approach can be applied to arbitrary graphs, in contrast to special cases for which poly-time algorithms have been found [ 16, 22 ] or unsatisfiability can be determined analytically [ 23, 24 ]. We evaluate this approach in two settings of particular interest [ 16, 24 ]: ifrst, we synthesize the ubiquitous Greenberger–Horne–Zeilinger (GHZ) state [ 25 ] from random graphs with varying number of qubits. Next, we target a 14 node quantum network proposal [ 26 ]. Within 30 minutes BMC finds transformations for graphs up to 17 nodes (qubits). In comparison, for transformations under single-qubit Cliford operations without measurements (a setting where deciding reachability is in P [ 27, 28 ] and counting reachable graphs is #P-complete [ 29 ]), various properties of equivalence classes have been explored up to 12 qubits [ 30, 31, 32 ].

Aside from graph problems which have been tackled with SAT-based methods [ 33, 34, 35, 36, 37, 38, 39, 40 ], SAT has also been used on problems in quantum computing. For example, synthesizing optimal Cliford circuits without measurements (closely related to graph-state synthesis under LC + flipping arbitrary edges, but without VD) has been tackled with BMC [ 41 ]. Without the optimality constraint (i.e. shortest circuit) this problem is in P [ 42 ], while the complexity with the optimality constraint is unknown. SAT-based techniques have also been applied to quantum circuit equivalence checking for a limited selection of circuits [ 43 ]. BMC specifically has been applied to Cliford circuit (without measurements) equivalence checking [ 44 ] (a problem that is also in P [ 45 ]), and SMT and planning based approaches have been used to map logical quantum circuits to physical quantum-chips [ 46, 47 ]. Unlike much previous work we include measurements, which for our problem raises the complexity from P to NP-complete. 2. Preliminaries and problem definition

2.1. Quantum computing

We very briefly introduce quantum bits (qubits) and how to act on them with quantum gates and measurements (see [ 48 ] for a complete introduction). The state | ⟩ of a single qubit ⎛ 00 01 . . . 0 ⎞ . . .

. .

. 0 1 . . . ⎟ . ⎠ | ⟩ = 0 |0⟩ + 1 |1⟩ = (︀ 0 1)︀ ⊺ for complex numbers 0, 1 satisfying | 0| is a complex 2-vector of unit norm, equalling the computational-basis states |0⟩ = (︀ 1 0)︀ ⊺ or |1⟩ = (︀ 0 1)︀ ⊺ or any linear combination of those, i.e. in general a single-qubit state is 2 + | 1|2 = 1 (here, ⊺ denotes vector transposition). A general -qubit quantum state is represented as a complex vector of length 2 with norm 1, e.g.

︁( 1 √ 2 )︁ ⊺ √ 2 and (︁ matrix ⊗ is states. The joint state of two separate quantum registers in states |⟩ , | ⟩ is |⟩ ⊗ | ⟩, where ⊗ denotes the tensor product: given × matrix and × matrix , the × ︁( 1 √ ⊗ (︀ 1 0)︀ ⊺ is not entangled, but √ Given a bipartition ∪ = {1, 2, . . . , }, an -qubit state | ⟩ is called separable over , if we can write | ⟩ = | ⟩ ⊗ | ⟩. It is entangled otherwise, a feature that has no classical analogue and is a prerequisite to many applications with a quantum advantage. For example

A quantum gate (always reversible) on qubits is given by a vector multiplication, for example (see right) which maps input 2 × 2 unitary matrix and the output state can be found by matrix- = is. = ︂( 1

0 )︂ 0 / 4 ⊗ = ⎜ ⎝ . . .

︂( 1 0)︂ gates in parallel to separate registers, e.g. ⊗ ⊗ is a 3-qubit gate performing a on the second qubit and on the first and third. The result of a two-qubit gate (e.g. controlled- (CZ ), which maps e.g.

2 . An example universal ) between two non-adjacent qubits can be computed by swapping qubits: e.g. for qubits 0, 1, 2, CZ (0, 2) = SWAP(1, 2)CZ (0, 1)SWAP(1, 2), where SWAP(1, 2) replaces |⟩⊗| ⟩⊗|

⟩ → |⟩⊗| ⟩⊗| ⟩ for , , ∈ {0, 1}. The gates , 2 together generate (under matrix multiplication and tensoring with ) the group of single-qubit Cliford gates , and , 2, CZ together generate all Cliford gates.

A computational-basis measurement is a non-reversible operation which projects a single |1⟩ ⊗ | 1⟩ where | |2 (| |2) is the probability of finding the first qubit in the qubit state 0 |0⟩ + 1 |1⟩ to one of |0⟩ , |1⟩ with probability | 0|2 or | 1|2. For example, measuring a qubit | ⟩ = √︀1/3 |0⟩ + √︀2/3 |1⟩ yields the state |0⟩ with probability 1/3 and the state |1⟩ with probability 2/3. Any -qubit state | ⟩ can be written as | ⟩ = |0⟩ ⊗ | 0⟩ + |0⟩ (|1⟩) state after measuring it (for expressing measurement on the other qubits, swap qubits first). A Pauli measurement equals a computational-basis measurement preceded by a single-qubit Cliford gate. Sequences of quantum operations are typically visualized in a quantum circuit (see Fig. 1).

2.2. Graph states and graph-state reachability

Graph states are a subset of all quantum states. An -qubit graph state |⟩ is represented by an undirected simple graph = (, ) with | | = vertices and no self-loops (where is | 1⟩ | 2⟩| 3⟩

| 4⟩ |0⟩ |0⟩ the vertex set and ⊆ × the edge set), constructed as starting from the state ⊗ |0⟩⊗ , followed by a CZ gate on each pair of qubits (, ) ∈ . An example is given in Fig. 2. From here on we say ‘graph’ to mean ‘undirected simple graph without self-loops’. Intuitively, the graph captures information about the entanglement between the qubits, where two qubits are entangled if they are (directly or indirectly) connected in the graph.

The two graph transformations corresponding to single-qubit quantum operations are: • Local complementation LC on vertex ∈ transforms = (, ) into () = (, ′) where ′ is obtained from by flipping the edges in the neighborhood of , i.e. for all , ∈ , if (, ) ∈ then (, ) ̸∈ ′ and if (, ) ̸∈ then (, ) ∈ ′. Here, the neighborhood is the set of all vertices adjacent to , i.e. = { | (, ) ∈ }. For any graphs and ′, |′⟩ is reachable from |⟩ using only single-qubit Cliford operations if and only if ′ is reachable from using local complementations. More specifically, the graph state |LC ()⟩ equals the resulting quantum state when applying a certain sequence of single-qubit Cliford operations to |⟩ (see [ 10 ] for details). • Vertex deletion VD of vertex ∈ transforms = (, ) to VD () = (, ′) with ′ = ∖ {(, ) | ∈ }, i.e. becomes isolated (all edges adjacent to are removed). Vertex deletion of vertex implements measurement on qubit : for each graph , the graph state |VD ()⟩ is single-qubit Cliford equivalent to |⟩ at which a computational-basis measurement has been performed on qubit [ 12 ].

And although not the primary focus of this work, we can also consider two-qubit operations: • Given a subset of pairs of nodes ⊆ × (for convenience < for (, ) ∈ ), can be transformed into ′ by edge flips among and local complementations on vertices in if and only if |⟩ can be transformed into |′⟩ using two-qubit Cliford operations on the qubit pairs in and single-qubit Cliford on qubits in [14-Th.1].

Rather than generating a graph state from scratch using CZ gates (as in Figs. 2a to 2c) a problem of interest for e.g. quantum networking is to obtain a particular graph from an existing graph using only single-qubit operations (LC+VD, and = ∅). Below is a practical example. Example 2.1. Alice is part of a 6-node quantum network and wants to run a quantum secret sharing scheme [ 9 ] between herself and three other parties, each having one qubit. For this she needs a 4-qubit Greenberger–Horne–Zeilinger (GHZ) state [ 25 ], given by GHZ on the right. However, generating |GHZ⟩ using CZ -gates (Figs. 2a to 2c)) requires generating entanglement [49, 50-Fig.2.4], which is a time-consuming probabilistic process [ 51 ]. At some point in time the network is a state |⟩. Because single-qubit operations (LC+VD on the graph) are much easier to perform than entanglement generation, Alice wants to know whether a given can be transformed into GHZ using only LC+VD.

B B

A GHZ

A

C D C D

This motivates the problem we will study in this work, posed before in [ 16 ] for single-qubit operations (LC+VD and = ∅) and in [ 14 ] for multi-qubit operations (LC+VD and ̸= ∅). Definition 2.1 (Graph-state synthesis). Given source and target graphs = (, ) and = (, ), find (if it exists) a sequence of local complementations and vertex deletions on any ∈ (and also edge flips on (, ) ∈ for some given ⊆ × in case multi-qubit Cliford operations are allowed on ) which transforms into .

We remark that if = × , any graph can be trivially synthesized because an edge may be added or removed between any pair of nodes (Figs. 2a to 2c). We also remark that we are not necessarily interested in the shortest sequence of graph transformations, as any sequence of LC+VD translates into at most one single-qubit Cliford and one measurement per qubit.

3. SAT encoding

As seen in the previous section, quantum operations on graph states can be expressed through graph transformations. In this section, we give Boolean encodings for these operations, as well as an encoding for the transition relation as a whole. The encoding of a single transformation step from graph to ′ uses variables ⃗ for and ⃗′ for ′. We encode a graph as follows. Definition 3.1 (Graph encoding). An undirected graph of vertices is encoded as a conjunction over ( − 1)/2 literals (¬), for (, ) ∈ U = {(, ) ∈ × | < }, indicating there is (not) an edge between nodes and .

3.1. Encoding of graph transformations

The Boolean encoding for deleting a vertex , denoted VD, is given in Eq. (1). All edges (, ) connected to are set to false (¬′) while all others remain unchanged (′ ↔ ).

VD =

⋀︁ (,)∈U {︃¬′ ′ ↔ if = or = otherwise.

(1)

The encoding for performing a local complementation on vertex , denoted LC, is given in Eq. (2) and can be read as follows: if vertices , are in the neighborhood of ( ∧ ) then the value of the edge (, ) is flipped ( ′ ↔ ¬(1 ⊕ ¬ ).

LC =

⋀︁ {︃′ ↔ ¬(( ∧ ) ⊕ ¬ )

In order to combine the transition relations LC, VD, and EF into a single CNF formula we use a construction similar to the BMC encoding of diferent concurrent threads in [ 52 ]: we add ⌈log2(max(| |, ||) + 1)⌉ variables ⃗ for the binary encoding of ∈ or ∈ {1, . . . , ||}, and two variables ⃗ to indicate whether a given operation is a local complementation (⃗ = 0), a vertex deletion (⃗ = 1), or an edge flip ( ⃗ = 2). For example the constraint ⃗ = 3 ∧ ⃗ = 1 represents vertex deletion of node 3. Using these additional variables, we encode all local complementations, vertex deletions, and edge flips as in Eqs. (4) to (6).

∈ ∈ ⋀︁ ∈{1,...,||} LC(⃗, ⃗′) = ⋀︁ [︁(⃗ = ∧ ⃗ = 0) → LC(⃗, ⃗′)]︁ VD(⃗, ⃗′) = ⋀︁ [︁(⃗ = ∧ ⃗ = 1) → VD(⃗, ⃗′)]︁ EF(⃗, ⃗′) = [︁(⃗ = ∧ ⃗ = 2) → EF(⃗, ⃗′)]︁ (2) (3) (4) (5) (6) (7)

Additionally we add an identity transition Id(⃗, ⃗′) = (⃗ = 3) → Id(⃗, ⃗′) to ensure that if a transformation of length exists, a transformation of length ′ ≥ also exists (to avoid searching over all ), and we appropriately constrain the unused values of ⃗ and ⃗ by adding = (⃗ < | | ∨ = 2) ∧ (⃗ < || ∨ ̸= 2). Finally, we obtain the the global transition relation in Eq. (7). When converted to CNF this formula has + ( − 1) variables and ≤ 3.53 + 22 + 0.52 + 0.5||2 clauses, where = | | and = ⌈log2(max(| |, ||) + 1)⌉.

global(⃗, ⃗′) = LC ∧ VD ∧ EF ∧ Id ∧

We use the transition relation specified in Eq. (7) in a bounded-model-checking set-up, i.e. we create Eq. (8) below, where (⃗1) encodes a source graph , (⃗) a target graph , and is the search depth.

− 1 (⃗1) ∧ ⋀︁ global(⃗, ⃗+1) ∧ (⃗) (8)

=1 The formula is satisfiable if and only if a sequence of operations of at most steps exists which transforms into . In Section 3.2, we prove an upper bound on the required depth .

3.2. Completeness threshold

To provide a completeness threshold for graph-state synthesis under LC+VD, we use the following observations to bound the search depth.

1. If can be transformed to ′ under LC, a transformation exists of at most local complementations, where = 3(| | − )/2 with = | |(mod 2) [27-§4]. 2. If can be transformed into under LC+VD, then vertex deletion needs to be performed on exactly the Δ vertices which are isolated in .1 3. For ∈ , after VD leaves the graph unchanged, i.e. LC (VD ()) = VD (). 4. For , ∈ and ̸= , and VD commute, i.e. LC (VD ()) = VD ( ()). From points 3 and 4, it follows that all vertex dele- |⟩ |′⟩ |⟩ tions (measurements) can be postponed until after the local complementations (single-qubit Cliford ignattoes).WunedtherenLCg+etVtDh,atitifcanbceantrabnestfroarnmsfeodrmbyeda | | } | | − Δ circuit of the form given in Fig. 3, taking at most Figure 3: Graph-state transformation circuit local complementations and Δ vertex deletions. under LC+VD.

4. Empirical evaluation

We evaluate our approach in two settings: synthesizing a GHZ state from random graphs for an increasing number of qubits, and synthesis of graphs based on a proposal of a 14 node quantum network in the Netherlands [ 26 ]. For all experiments, we perform binary search over up to the completeness threshold specified in Section 3.2. In our current setup, the solver is restarted for every diferent . Experiments2 were run on Ubuntu 18 with an AMD Ryzen 7 5800x CPU. Two diferent SAT solvers, Glucose 4 [ 53 ] and Kissat [ 54 ], have been used.

We first evaluate our approach in a setting where the target states are 4-qubit GHZ states (see Example 2.1), matching the target states in the empirical evaluation in [ 16 ]. GHZ states are used in a large number of applications such as quantum secret sharing [ 9 ] (see also Example 2.1), anonymous transfer [ 55 ] and conference key agreement [ 56 ]. The polynomial time algorithm presented in [ 16 ] can only be applied when the source graph has special properties (specifically it needs to have rank-width 1). To evaluate our method we replace the restricted random graphs used in [ 16 ] with more general Erdős-Rényi random graphs, which have also been used in other work concerning graph-state synthesis [57, 58]. Results are shown in Fig. 4. With a timeout of 30 minutes Kissat can synthesize transformations for graphs up to 17 qubits. Determining unreachability, which we do using the completeness threshold, can be done up to 8 qubits by Glucose within this timeout.

Next, we evaluate our approach on the specific quantum network architecture proposed in [26-Fig.3] (visualized in Fig. 5a). As source states, we consider graphs with nodes from this network, and random edges as follows: (, ) ∈ with probability , where is the distance 1Without loss of generality, we assume has no isolated vertices. If has isolated vertices which are not isolated in , then is trivially unreachable under LC+VD. 2Reproducible experiments are available online at https://github.com/sebastiaanbrand/graph-state-synthesis. sat, kissat sat, glu4 unsat, kissat unsat, glu4 (number of hops + 1) between the nodes, motivated by the fact that generating entanglement over larger distances is harder [ 51 ]. The target state is a GHZ state between the main network nodes (squares in Figure 5a). Fig. 5b shows the results for varying . A higher corresponds to a larger amount of entanglement in the network. We observe that for fixed number of nodes, the time it takes to synthesize a transformation increases with the density of the source graph.

Acknowledgments

This work was supported by the NEASQC project, funded by European Union’s Horizon 2020, Grant Agreement No. 951821, and by the Dutch National Growth Fund, as part of the Quantum Delta NL programme.

Physical Review A 97 (2018) 022307. [57] B. Li, S. E. Economou, E. Barnes, Photonic resource state generation from a minimal number of quantum emitters, npj Quantum Information 8 (2022) 11. [58] S.-H. Lee, H. Jeong, Graph-theoretical optimization of fusion-based graph state generation, arXiv preprint arXiv:2304.11988 (2023).

References

[1] C. H. Bennett , G. Brassard, Quantum cryptography: Public key distribution and coin tossing , Proceedings of IEEE International Conference on Computers, Systems and Signal Processing 175 ( 1984 ). doi: 10 .1016/j.tcs. 2014 . 05 .025.

[2] A. K. Ekert , Quantum cryptography based on Bell's theorem , Phys. Rev. Lett . 67 ( 1991 ) 661 - 663 . URL: http://link.aps.org/doi/10.1103/PhysRevLett.67.661. doi: 10 .1103/ PhysRevLett.67.661.

[3] R. Jozsa , D. S. Abrams , J. P. Dowling , C. P. Williams , Quantum clock synchronization based on shared prior entanglement , Physical Review Letters 85 ( 2000 ) 2010 .

[4] Y. Cao , J. Romero , J. P. Olson , M. Degroote , P. D. Johnson , M. Kieferová , I. D. Kivlichan , T. Menke , B. Peropadre , N. P. D. Sawaya , S. Sim , L. Veis , A. Aspuru-Guzik , Quantum chemistry in the age of quantum computing , Chemical Reviews 119 ( 2019 ) 10856 - 10915 . URL: https://doi.org/10.1021/acs.chemrev.8b00803. doi: 10 .1021/acs.chemrev.8b00803.

[5] M. Hein , W. Dür , J. Eisert , R. Raussendorf , M. Nest , H. - J. Briegel , Entanglement in graph states and its applications , arXiv preprint quant-ph/0602096 ( 2006 ).

[6] R. Raussendorf , H. J. Briegel , A one-way quantum computer , Phys. Rev. Lett . 86 ( 2001 ) 5188 - 5191 . URL: https://link.aps.org/doi/10.1103/PhysRevLett.86.5188. doi: 10 . 1103/PhysRevLett.86.5188.

[7] S. Anders , H. J. Briegel , Fast simulation of stabilizer circuits using a graph-state representation , Physical Review A 73 ( 2006 ) 022334 .

[8] D. Gottesman , Stabilizer codes and quantum error correction , arXiv:quant-ph/9705052 ( 1997 ).

[9] M. Hillery , V. Bužek , A. Berthiaume , Quantum secret sharing, Physical Review A 59 ( 1999 ) 1829 .

[10] M. Van den Nest , J. Dehaene , B. De Moor, Graphical description of the action of local Cliford transformations on graph states , Phys. Rev. A 69 ( 2004 ) 022316 . doi: 10 .1103/ PhysRevA.69.022316.

[11] M. Van den Nest , Local equivalence of stabilizer states and codes ( phd thesis) ( 2005 ).

[12] M. Hein , J. Eisert , H. J. Briegel , Multiparty entanglement in graph states , Physical Review A 69 ( 2004 ) 062311 .

[13] Z. Ji , J. Chen , Z. Wei , M. Ying , The lu-lc conjecture is false , arXiv preprint arXiv:0709.1266 ( 2007 ).

[14] M. Englbrecht , T. Kraft , B. Kraus , Transformations of stabilizer states in quantum networks , Quantum 6 ( 2022 ) 846 .

[15] A. Dahlberg , S. Wehner , Transforming graph states using single-qubit operations , Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 376 ( 2018 ) 20170325 .

[16] A. Dahlberg , J. Helsen , S. Wehner , How to transform graph states using single-qubit operations: computational complexity and algorithms , Quantum Science and Technology 5 ( 2020 ) 045016 .

[17] A. Dahlberg , J. Helsen , S. Wehner , Transforming graph states to Bell-pairs is NP-complete , Quantum 4 ( 2020 ) 348 .

[18] B. Courcelle , S.-i. Oum, Vertex-minors, monadic second-order logic, and a conjecture by seese , Journal of Combinatorial Theory, Series B 97 ( 2007 ) 91 - 126 .

[19] B. Courcelle , J. Engelfriet , Graph Structure and Monadic Second-Order Logic : A LanguageTheoretic Approach , Encyclopedia of Mathematics and its Applications , Cambridge University Press, 2012 . doi: 10 .1017/CBO9780511977619.

[20] E. Clarke , A. Biere , R. Raimi , Y. Zhu , Bounded model checking using satisfiability solving, Formal methods in system design 19 ( 2001 ) 7 - 34 .

[21] A. Biere , A. Cimatti , E. M. Clarke , O. Strichman , Y. Zhu , Bounded model checking ., in: Handbook of satisfiability, IOS press, 2009 , pp. 457 - 481 .

[22] F. Hahn , A. Pappa , J. Eisert , Quantum network routing and local complementation , npj Quantum Information 5 ( 2019 ) 76 .

[23] F. Hahn , A. Dahlberg , J. Eisert , A. Pappa , Limitations of nearest-neighbor quantum networks , Physical Review A 106 ( 2022 ) L010401 .

[24] J. de Jong , F. Hahn, N. Tcholtchev , M. Hauswirth , A. Pappa , Extracting maximal entanglement from linear cluster states , arXiv preprint arXiv:2211.16758 ( 2022 ).

[25] D. M. Greenberger , M. A. Horne , A. Zeilinger , Going beyond bell's theorem, in: Bell's theorem, quantum theory and conceptions of the universe , Springer, 1989 , pp. 69 - 72 .

[26] J. Rabbie , K. Chakraborty , G. Avis, S. Wehner , Designing quantum networks using preexisting infrastructure , npj Quantum Information 8 ( 2022 ) 5 .

[27] A. Bouchet , An eficient algorithm to recognize locally equivalent graphs , Combinatorica 11 ( 1991 ) 315 - 329 .

[28] M. van den Nest , J. Dehaene , B. de Moor, Eficient algorithm to recognize the local Cliford equivalence of graph states , Physical Review A 70 ( 2004 ) 034302 .

[29] A. Dahlberg , J. Helsen , S. Wehner , Counting single-qubit Cliford equivalent graph states is #P-complete , Journal of Mathematical Physics 61 ( 2020 ) 022202 .

[30] L. E. Danielsen , M. G. Parker , On the classification of all self-dual additive codes over gf (4) of length up to 12 , Journal of Combinatorial Theory, Series A 113 ( 2006 ) 1351 - 1367 .

[31] A. Cabello , L. E. Danielsen , A. J. López-Tarrida , J. R. Portillo , Optimal preparation of graph states , Physical Review A 83 ( 2011 ) 042314 .

[32] J. C. Adcock , S. Morley-Short , A. Dahlberg , J. W. Silverstone , Mapping graph state orbits under local complementation , Quantum 4 ( 2020 ) 305 .

[33] M. J. Heule , S. Szeider , A SAT approach to clique-width, ACM Transactions on Computational Logic (TOCL) 16 ( 2015 ) 1 - 27 .

[34] M. Samer , H. Veith , Encoding treewidth into SAT, in: Theory and Applications of Satisfiability Testing-SAT 2009 : 12th International Conference, SAT 2009, Swansea , UK , June 30-July 3, 2009 . Proceedings 12, Springer, 2009 , pp. 45 - 50 .

[35] A. Schidler , S. Szeider , A SAT approach to twin-width , in: 2022 Proceedings of the Symposium on Algorithm Engineering and Experiments , SIAM , 2022 , pp. 67 - 77 .

[36] R. Ganian , N. Lodha , S. Ordyniak , S. Szeider, SAT-encodings for treecut width and treedepth , in: 2019 Proceedings of the Twenty-First Workshop on Algorithm Engineering and Experiments , SIAM , 2019 , pp. 117 - 129 .

[37] N. Lodha , S. Ordyniak , S. Szeider, SAT-encodings for special treewidth and pathwidth, in: Theory and Applications of Satisfiability Testing-SAT 2017 : 20th International Conference, Melbourne, VIC , Australia, August 28-September 1 , 2017 , Proceedings 20, Springer, 2017 , pp. 429 - 445 .

[38] N. Lodha , S. Ordyniak , S. Szeider , A SAT approach to branchwidth, in: Theory and Applications of Satisfiability Testing-SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8 , 2016 , Proceedings 19, Springer, 2016 , pp. 179 - 195 .

[39] N. Lodha , S. Ordyniak , S. Szeider , A SAT approach to branchwidth, ACM Transactions on Computational Logic (TOCL) 20 ( 2019 ) 1 - 24 .

[40] B. Courcelle , I. A. Durand , On using SAT solvers for graph computations ( 2022 ).

[41] S. Schneider , L. Burgholzer , R. Wille , A SAT encoding for optimal Cliford circuit synthesis , in: Proceedings of the 28th Asia and South Pacific Design Automation Conference , 2023 , pp. 190 - 195 .

[42] S. Aaronson , D. Gottesman , Improved simulation of stabilizer circuits , Physical Review A 70 ( 2004 ) 052328 .

[43] S. Yamashita , I. L. Markov , Fast equivalence-checking for quantum circuits , in: 2010 IEEE/ACM International Symposium on Nanoscale Architectures , IEEE, 2010 , pp. 23 - 28 .

[44] L. Berent , L. Burgholzer , R. Wille , Towards a SAT encoding for quantum circuits: A journey from classical circuits to Cliford circuits and beyond , arXiv:2203.00698 ( 2022 ).

[45] M. Amy , Towards large-scale functional verification of universal quantum circuits , arXiv preprint arXiv: 1805 . 06908 ( 2018 ).

[46] B. Tan , J. Cong , Optimal layout synthesis for quantum computing , in: Proceedings of the 39th International Conference on Computer-Aided Design , 2020 , pp. 1 - 9 .

[47] I. Shaik , J. van de Pol, Optimal layout synthesis for quantum circuits as classical planning , arXiv preprint arXiv:2304.12014 ( 2023 ).

[48] M. A. Nielsen , I. Chuang , Quantum computation and quantum information, American Association of Physics Teachers, 2002 .

[49] J. Eisert , K. Jacobs , P. Papadopoulos , M. B. Plenio , Optimal local implementation of nonlocal quantum gates , Physical Review A 62 ( 2000 ) 052317 .

[50] N. Nickerson , Practical fault-tolerant quantum computing ., Ph.D. thesis , Imperial College London, 2015 .

[51] N. Sangouard , C. Simon , H. de Riedmatten, N. Gisin, Quantum repeaters based on atomic ensembles and linear optics , Rev. Mod. Phys . 83 ( 2011 ) 33 - 80 . URL: https://link.aps.org/ doi/10.1103/RevModPhys.83.33. doi: 10 .1103/RevModPhys.83.33.

[52] I. Rabinovitz , O. Grumberg , Bounded model checking of concurrent programs , in: Computer Aided Verification: 17th International Conference, CAV 2005, Edinburgh, Scotland, UK , July 6- 10 , 2005 . Proceedings 17, Springer, 2005 , pp. 82 - 97 .

[53] G. Audemard , L. Simon , On the Glucose SAT solver , International Journal on Artificial Intelligence Tools 27 ( 2018 ) 1840001 .

[54] A. Biere , M. Fleury , Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022 , in: T. Balyo, M. Heule , M. Iser , M. Järvisalo , M. Suda (Eds.), Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions , volume B- 2022 -1 of Department of Computer Science Series of Publications B, University of Helsinki, 2022 , pp. 10 - 11 .

[55] M. Christandl , S. Wehner , Quantum anonymous transmissions , in: Advances in CryptologyASIACRYPT 2005: 11th International Conference on the Theory and Application of Cryptology and Information Security , Chennai, India, December 4- 8 , 2005 . Proceedings 11, Springer, 2005 , pp. 217 - 235 .

[56] J. Ribeiro , G. Murta, S. Wehner , Fully device-independent conference key agreement,