IP Library › Granted Patent US 12,705,515
Granted Patent B1
US 12,705,515 · App. 17/694,381 · Granted Aug 11, 2026

Finding clifford circuit solutions using SMT solvers

Inventors: Noah John Shutty (Redwood City, CA); Christopher Chamberland (Pasadena, CA)
Assignee: Amazon Technologies, Inc.
G06N10/20G06N10/60G06N10/70
View Patent ↗
Loading inventors, assignments & file history…
Monitor This Case
Get email alerts when status or documents change.
Order Certified Copies
Most orders are placed with the USPTO same day — all within 24 business hours.
Order via The Patent Place →
Pre-filled with this patent's details
Quick Facts
Patent No.
US 12,705,515
App. No.
17/694,381
Filed
Mar 14, 2022
Granted
Aug 11, 2026
Kind
B1
Art Unit
2128
USPC
706/62
Abstract

A technique for deriving Clifford circuits using a Satisfiability Modulo Theories (SMT) solver via encoding a Clifford circuit design problem as an SMT decision problem is disclosed. Both symbolic bit matrix representations of elements of the Clifford circuit design problem and constraint equations for modeling the Clifford circuit are used to construct an encoded SMT solver protocol. Clifford circuit solutions are then solved for by the SMT solver before one or more of the solutions are implemented into quantum hardware. Such a technique can be applied to bottom-up fault-tolerant magic state preparation protocol such that an encoded magic state can be teleported from a color code to a surface code via lattice surgery, resulting in a merged surface and color code. Decoding the stabilizer measurements of the merged code requires a decoding algorithm specific to error correction of the merged code.

Claims (66)

1 . A method, comprising:

encoding a Clifford circuit design problem as a Satisfiability Modulo Theories (SMT) decision problem, wherein said encoding the Clifford circuit design problem as the SMT decision problem comprises:

determining one or more symbolic bit matrix representations for one or more elements of the Clifford circuit design problem;

determining one or more constraint equations for modeling one or more Clifford circuits; and

constructing an encoded SMT protocol for the SMT decision problem, based at least in part on:

the determined one or more symbolic bit matrix representations; and

the determined one or more constraint equations;

providing the encoded SMT protocol to an SMT solver;

returning one or more Clifford circuit solutions found by the SMT solver; and

implementing the one or more Clifford circuit solutions on a quantum hardware device.

2 . The method of claim 1 , wherein the Clifford circuit design problem is to implement a quantum algorithm.

3 . The method of claim 1 , wherein the Clifford circuit design problem is to implement a quantum error-correcting code.

4 . The method of claim 1 , wherein the one or more elements of the Clifford circuit design problem of which respective symbolic bit matrix representations are determined comprise:

a plurality of qubits; and

a plurality of gates acting on one or more respective qubits of the plurality of qubits,

wherein the plurality of qubits and the plurality of gates are used to implement a quantum error-correcting code to be executed within a given number of time steps.

5 . The method of claim 4 , wherein the Clifford circuit design problem comprises gate connectivity information for the layout of the plurality of qubits in the quantum error-correcting code.

6 . The method of claim 4 , wherein the constraint equations for modeling the one or more Clifford circuits comprise a constraint wherein the constraint is that respective qubits of the plurality of qubits are assigned one respective functionality from a plurality of functionalities, the functionalities comprising two or more of: a data qubit, an ancilla qubit, a root ancilla qubit, or a flag qubit.

7 . The method of claim 4 , wherein the constraint equations for modeling the one or more Clifford circuits comprise a further constraint wherein the further constraint is that at most one gate is assigned to act on a given respective qubit of the plurality of qubits at any given time step of the number of time steps.

8 . The method of claim 4 , wherein the Clifford circuit design problem is a Clifford circuit design problem for determining one or more Hadamard (|H -type) magic states implemented via the one or more Clifford circuits in the quantum error-correcting code, wherein the quantum error-correcting code comprises a quantum color code.

9 . The method of claim 8 , wherein the one or more Clifford circuits that implement one or more Hadamard (|H -type) magic states are prepared via measuring a logical Hadamard operator of the quantum color code and performing at least one round of X or Z stabilizer measurements for error detection.

10 . The method of claim 9 , wherein the constraint equations for modeling the one or more Clifford circuits comprise a further constraint wherein:

respective qubits of the plurality of qubits are assigned one respective functionality from a plurality of functionalities, the functionalities comprising a data qubit, an ancilla qubit, a root ancilla qubit, and a flag qubit; and

at most one qubit of the plurality of qubits is assigned the functionality of root ancilla qubit.

11 . The method of claim 1 , wherein the SMT protocol is further configured to exclude candidate Clifford circuit solutions that do not include a v-flag, wherein a non-trivial measurement of the v-flag indicates a presence of a number of errors greater than a given threshold.

12 . The method of claim 1 , wherein said returning the one or more Clifford circuit solutions further comprises:

verifying that one or more Clifford circuit solutions found by the SMT solver do not satisfy a v-flag property; and

wherein the method further comprises:

in response to the one or more Clifford circuit solutions found by the SMT solver not satisfying the v-flag property, adding one or more additional constraint equations to the Clifford circuit design problem;

constructing an updated encoded SMT protocol for an updated version of the Clifford circuit design problem that includes the added one or more additional constraint equations; and

providing the updated encoded SMT protocol to the SMT solver,

wherein the method comprises iteratively performing said verifying, said adding one or more additional constraint equations, and said repeating the constructing of respective updated encoded SMT protocols and said providing of the respective updated encoded SMT protocols to the SMT solver until one or more Clifford circuit solutions are returned that satisfy the v-flag property.

13 . The method of claim 1 , wherein the one or more Clifford circuit solutions implemented on the quantum hardware device are implemented on a quantum color code, and said quantum color code is merged with a quantum surface code on the quantum hardware device.

14 . The method of claim 13 , wherein the quantum color code merged with the quantum surface code is decoded using a decoder for correcting one or more errors for a merged surface and color quantum code.

15 . A system, comprising:

one or more computing devices configured to:

encode a Clifford circuit design problem as a Satisfiability Modulo Theories (SMT) decision problem, wherein said encode the Clifford circuit design problem as the SMT decision problem comprises:

determining one or more symbolic bit matrix representations for one or more elements of the Clifford circuit design problem;

determining one or more constraint equations for modeling one or more Clifford circuits; and

constructing an encoded SMT protocol for the SMT decision problem, based at least in part on:

the determined one or more symbolic bit matrix representations; and

the determined constraint equations for modeling the one or more Clifford circuits;

provide the encoded SMT protocol to an SMT solver; and

cause one or more Clifford circuit solutions found by the SMT solver to be implemented on a quantum hardware device.

16 . The system of claim 15 , wherein the one or more elements of the Clifford circuit design problem of which respective symbolic bit matrix representations are determined comprise:

a plurality of qubits; and

a plurality of gates acting on one or more respective qubits of the plurality of qubits,

wherein the plurality of qubits and the plurality of gates are used to implement a quantum error-correcting code to be executed within a given number of time steps.

17 . The system of claim 16 , wherein the SMT protocol is further configured to exclude candidate Clifford circuit solutions that do not include a v-flag, wherein a non-trivial measurement of the v-flag indicates a presence of a number of errors greater than a given threshold.

18 . The system of claim 15 , further comprising:

the one or more computing devices further configured to:

provide the encoded SMT protocol to an SMT solver; and

return one or more Clifford circuit solutions found by the SMT solver; and

one or more quantum hardware devices configured to:

implement the one or more Clifford circuit solutions.

19 . A non-transitory, computer-readable, medium storing program instructions that, when executed on or across one or more processors, cause the one or more processors to:

encode a Clifford circuit design problem as a decision problem, wherein said encode the Clifford circuit design problem as the decision problem comprises:

determining one or more symbolic bit matrix representations for one or more elements of the Clifford circuit design problem;

determining one or more constraint equations for modeling one or more Clifford circuits; and

constructing an encoded protocol for the decision problem, based at least in part on:

the determined one or more symbolic bit matrix representations; and

the determined one or more constraint equations;

provide the encoded protocol to a solver; and

cause one or more Clifford circuit solutions found by the solver to be implemented on a quantum hardware device.

20 . The non-transitory, computer-readable medium of claim 19 , wherein to encode the Clifford circuit design problem as the decision problem, the program instructions further cause the one or more processors to:

implement a quantum error-correcting code comprising a plurality of qubits and a plurality of gates acting on one or more respective qubits of the plurality of qubits to be executed within a given number of time steps.

Assignments (1)
ASSIGNMENT OF ASSIGNOR'S INTEREST Recorded Mar 17, 2022
From: SHUTTY, NOAH JOHN; CHAMBERLAND, CHRISTOPHER
To: AMAZON TECHNOLOGIES, INC.
Reel/Frame 059291/0067 →
Continuity (1)
Provisional Application 63299854 · Jan 14, 2022
References Cited (71)
US 10248491B1 · Zeng · 2019 [cited by applicant]
US 10352992B1 · Zeng · 2019 [cited by applicant]
US 11567827B2 · Zheng · 2023 [cited by examiner]
US 11748652B1 · Kubica · 2023 [cited by applicant]
US 20110246831A1 · Das · 2011 [cited by examiner]
US 20190044543A1 · Chamberland · 2019 [cited by applicant]
US 20200348579A1 · Heuck · 2020 [cited by applicant]
US 20210374588A1 · Gidney · 2021 [cited by applicant]
US 20210398009A1 · Vuletic · 2021 [cited by applicant]
US 20210406755A1 · Martiel · 2021 [cited by examiner]
US 20220222567A1 · Reagor · 2022 [cited by applicant]
US 20220404533A1 · Zhou · 2022 [cited by examiner]
US 20230071000A1 · Higgott · 2023 [cited by applicant]
US 20230162081A1 · Verresen · 2023 [cited by applicant]
Litinkski et al. “Lattice Surgery with a Twist: Simplifying Clifford Gates of Surface Codes,” Apr. 17, 2018, Quantum, pp. 1-16. (Year: 2018). [cited by examiner]
Landahl et al. “Quantum computing by color-code lattice surgery,” Jul. 18, 2014, Quantum, pp. 1-13. (Year: 2014). [cited by examiner]
A. Kubica and N. Delfosse, “Efficient color code decoders in d > 2 dimensions from toric code decoders,” arXiv e-prints (2019), 1905.07393 [quant-ph], pp. 1-28. [cited by applicant]
J. Edmonds, “Paths, trees, and flowers,” Canadian Journal of mathematics 17, pp. 449-467 (1965). [cited by applicant]
V. Strassen, “Gaussian elimination is not optimal, ” Numerische mathematik, vol. 13, issue 4, pp. 354-356 (1969). [cited by applicant]
S. Bravyi and D. Gosset, “Improved Classical Simulation of Quantum Circuits Dominated by Clifford Gates,” Phys. Rev. Lett. 116, 250501 (2016 American Physical Society, pp. 1-5). [cited by applicant]
U.S. Appl. No. 17/694,399, filed Mar. 14, 2022, Noah John Shutty, et al. [cited by applicant]
T. J. Yoder and I. H. Kim, :The surface code with a twist, Quantum vol. 1, p. 2 (2017), arXiv:1612.04795v2, pp. 1-19. [cited by applicant]
D. Litinski and F. v. Oppen, Lattice Surgery with a Twist: Simplifying Clifford Gates of Surface Codes, Quantum vol. 2, p. 62 (2018), arXiv:1709.02318v2, pp. 1-16. [cited by applicant]
C. Chamberland, A. Kubica, T. J. Yoder, and G. Zhu, “Triangular color codes on trivalent graphs with flag qubits”, New Journal of Physics, vol. 22, 023019, (2020), pp. 1-24. [cited by applicant]
P. Prabhu and B. W. Reichardt, “Fault-tolerant syndrome extractionand cat state preparation with fewer qubits”, (2021). 2108.02184 [quant-ph], arxiv.org/abs/2108.02184, pp. 1-10. [cited by applicant]
A. M. Steane, “Overhead and noise threshold of fault-tolerant quantum error correction”, Phys. Rev. A 68, 042322 (2003), arxiv.org/abs/quant-ph/0207119v4, pp. 1-21. [cited by applicant]
E. Knill, “Quantum computing with realistically noisy devices”, Nature Publishing Group, vol. 434, pp. 39-44 (2005). [cited by applicant]
P. Aliferis, D. Gottesman, and J. Preskill, “Quantum accuracy threshold for concatenated distance-3 codes”, Quant. Inf. Comput. 6, 97 (2006) arxiv.org/pdf/quant-ph/0504218.pdf, pp. 1-58. [cited by applicant]
R. Chao and B. W. Reichardt, “Quantum error correction with only two extra qubits”, Phys. Rev. Lett. 121, 050502 (2018), preprint: https://arxiv.org/pdf/1705.02329.pdf, pp. 1-9. [cited by applicant]
R. Chao and B. W. Reichardt, “Fault-tolerant quantum computation with few qubits”, npj Quantum Information 4, 42 (2018), pp. 1-8. [cited by applicant]
C. Chamberland and M. E. Beverland, “Flag fault-tolerant error correction with arbitrary distance codes”, Quantum vol. 2, p. 53, 2018, arXiv:1708.02246v3, pp. 1-29. [cited by applicant]
T. Tansuwannont, C. Chamberland, and D. Leung, “Flag fault-tolerant error correction, measurement, and quantum computation for cyclic Calderbank-Shor-Steane codes”, Phys. Rev. A 101, 012342 (2020), arXiv:1803.09758v3, p… [cited by applicant]
B. W. Reichardt, “Fault-tolerant quantum error correction for steane's seven-qubit color code with few or no extra qubits,” Quantum Science and Technology 6, 015007 (2020), arXiv:1804.06995v1, pp. 1-11. [cited by applicant]
C. Chamberland, G. Zhu, T. J. Yoder, J. B. Hertzberg, and A. W. Cross, “Topological and subsystem codes on low-degree graphs with flag qubits,” Published by the American Physical Society, Phys. Rev. X 10, 011022 (2020),… [cited by applicant]
R. Chao and B.W. Reichardt, “Flag fault-tolerant error correction for any stabilizer code”, Published by the American Physical Society, PRX Quantum 1, 010302 (2020), pp. 1-6. [cited by applicant]
T. Tansuwannont and D. Leung, “Fault-tolerant quantum error correction using error weight parities,” arXiv e-prints , arXiv:2006.03068 (2020), arXiv:2006.03068 [quant-ph], pp. 1-13. [cited by applicant]
T. Tansuwannont and D. Leung, “Achieving fault tolerance on capped color codes with few ancillas”, arXiv e-prints , arXiv:2106.02649 (2021), arXiv:2106.02649 [quant-ph], pp. 1-39. [cited by applicant]
C. Chamberland and A. W. Cross, “Fault-tolerant magic state preparation with flag qubits”, Quantum 3, 143 (2019), arXiv e-prints arXiv:1811.00566v2 , pp. 1-26. [cited by applicant]
C. Chamberland and K. Noh, “Very low overhead fault-tolerant magic state preparation using redundant ancilla encoding and flag qubits,” npj Quantum Information 6, 1 (2020), arXiv preprint arXiv:2003.03049, ages 1-27. [cited by applicant]
L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in International conference on Tools and Algorithms for the Construction and Analysis of Systems (Springer, 2008) pp. 337-340. [cited by applicant]
H. Bombin and M. A. Martin-Delgado, “Topological quantum distillation,” Phys. Rev. Lett. 97, 180501 (2006), arXiv breprint arXiv:quant-ph/0605138, pp. 1-4. [cited by applicant]
H. Bombín, “Gauge color codes: optimal transversal gates and gauge fixing in topological stabilizer codes,” New Journal of Physics 17, 083002, IOP Publishing Ltd (2015), pp. 1-14. [cited by applicant]
A. Kubica and M. E. Beverland, “Universal transversal gates with color codes: A simplified approach,” Phys. Rev. A 91, 032330 (2015), arXiv preprint: arxiv.org/abs/1410.0069, pp. 1-13. [cited by applicant]
F. Thomsen, M. S. Kesselring, S. D. Bartlett, and B. J. Brown, “Low-overhead quantum computing with the color code,” (2022), 2201.07806 [quant-ph], pp. 1-8. [cited by applicant]
A. Y. Kitaev, “Fault-tolerant quantum computation by anyons,” Annals of Physics vol. 303, Issue 1, (2003), arXiv preprint: arxiv.org/pdf/quant-ph/9707021.pdf, pp. 1-27. [cited by applicant]
S. B. Bravyi and A. Y. Kitaev, “Quantum codes on a lattice with boundary,” arXiv e-prints: arxiv.org/pdf/quant-ph/9811052 (1998), pp. 1-6. [cited by applicant]
E. Dennis, A. Kitaev, A. Landahl, and J. Preskill, “Topological quantum memory,” Journal of Mathematical Physics 43, 4452, arXiv e-prints: arXiv:quant-ph/0110143v1 (2002), pp. 1-39. [cited by applicant]
A. G. Fowler, M. Mariantoni, J. M. Martinis, and A. N. Cleland, “Surface codes: Towards practical large-scale quantum computation,” Phys. Rev. A 86, 032324 (American Physical Society 2012), pp. 1-48. [cited by applicant]
J. P. B. Ataides, D. K. Tuckett, S. D. Bartlett, S. T. Flammia, and B. J. Brown, “The xzzx surface code,” Nature communications 12, 1 (2021), pp. 1-13. [cited by applicant]
C. Chamberland, K. Noh, P. Arrangoiz-Arriola, E. T. Campbell, C. T. Hann, J. Iverson, H. Putterman, T. C. Bohdanowicz, S. T. Flammia, A. Keller, G. Refael, J. Preskill, L. Jiang, A. H. Safavi-Naeini, O. Painter, and F. … [cited by applicant]
H. Bombin, C. Dawson, R. V. Mishmash, N. Nickerson, F. Pastawski, and S. Roberts, “Logical blocks for fault-tolerant topological quantum computation,” (2021), 2112.12160 [quantph], pp. 1-34. [cited by applicant]
C. Barrett and C. Tinelli, “Satisfiability Modulo Theories,” in Handbook of model checking (Springer, 2018) pp. 1-41. [cited by applicant]
J. Backes, S. Bayless, B. Cook, C. Dodge, A. Gacek, A. J. Hu, T. Kahsai, B. Kocik, E. Kotelnikov, J. Kukovec, et al., “Reachability Analysis for AWS-Based Networks,” in International Conference on Computer Aided Verific… [cited by applicant]
L. De Moura and N. Bjørner, “Satisfiability modulo theories: introduction and applications,” Communications of the ACM vol. 54, Issue 9, pp. 69-77 (2011). [cited by applicant]
T. Weber, S. Conchon, D. D'eharbe, M. Heizmann, A. Niemetz, and G. Reger, “The SMT competition 2015-2018,” Journal on Satisfiability, Boolean Modeling, and Computation 11 (2019), pp. 1-39. [cited by applicant]
T. Balyo, M. Heule, and M. Jarvisalo, “Sat competition 2016: Recent developments,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 31 (2017), pp. 1-3. [cited by applicant]
B. Tan and J. Cong, Optimal layout synthesis for quantum computing, in Proceedings of the 39th International Conference on Computer-Aided Design, ICCAD '20 (Association for Computing Machinery, New York, NY, USA, 2020),… [cited by applicant]
J. Ding and S. Yamashita, “Exact synthesis of nearest neighbor compliant quantum circuits in 2-d architecture and its application to large-scale circuits,” IEEE Transactions on Computer-Aided Design of Integrated Circui… [cited by applicant]
P. Murali, A. Javadi-Abhari, F. T. Chong, and M. Martonosi, “Formal constraint-based compilation for noisy Intermediate-scale quantum systems,” ELSEVIER, Microprocessors and Microsystems 66, 102 (2019), arXiv preprint: … [cited by applicant]
P. Murali, J. M. Baker, A. Javadi-Abhari, F. T. Chong, and M. Martonosi, “Noise-Adaptive Compiler Mappings for Noisy Intermediate-Scale Quantum Computers,” in Proceedings of the Twenty-Fourth International Conference on… [cited by applicant]
H. P. Nautrup, N. Friis, and H. J. Briegel, “Fault-tolerant interface between quantum memories and quantum processors,” Nature communications 8, 1 (2017), pp. 1-8. [cited by applicant]
S. Bravyi and A. Kitaev, “Universal quantum computation with ideal clifford gates and noisy ancillas, ” Phys. Rev. A 71, 022316, (2005 The American Physical Society), pp. 1-14. [cited by applicant]
A. Paetznick and B. W. Reichardt, “Universal Fault-Tolerant Quantum Computation with Only Transversal Gates and Error Correction”, Phys. Rev. Lett. 111, 090505 (2013), arXiv preprint: arxiv.org/abs/1304.3709, pp. 1-5. [cited by applicant]
J. T. Anderson, G. Duclos-Cianci, and D. Poulin, “Fault-Tolerant Conversion between the Steane and Reed-Muller Quantum Codes,” Phys. Rev. Lett. 113, 080501 (2014), arXiv preprint: arXiv:1403.2734v1, pp. 1-6. [cited by applicant]
H. Bombin, “Dimensional jump in quantum error correction,” New Journal of Physics, 18, IOP Institute of Physics, 043038 (2016 6 IOP Publishing Ltd), pp. 1-13. [cited by applicant]
D. Litinski, “Magic State Distillation: Not as Costly as You Think,” Quantum vol. 3, p. 205 (2019), arXiv preprint: arXiv:190.06903v3, pp. 1-22. [cited by applicant]
M. E. Beverland, A. Kubica, and K. M. Svore, “Cost of Universality: A Comparative Study of the Overhead of State Distillation and Code Switching with Color Codes,” PRX Quantum 2, 020341, Published by the American Physic… [cited by applicant]
D. Litinski, “A Game of Surface Codes: Large-Scale Quantum Computing with Lattice Surgery,” Quantum vol. 3, 128 (2019), arXiv:1808.02892v3, pp. 1-37. [cited by applicant]
A. G. Fowler and C. Gidney, “Low overhead quantum computation using lattice surgery”, arXiv e-prints (2018), 1808.06709 [quant-ph], pp. 1-15. [cited by applicant]
C. Chamberland and E. T. Campbell, “Universal quantum computing with twist-free and temporally encoded lattice surgery,” arXiv e-prints (2021), 2109.02746 [quant-ph], pp. 1-23. [cited by applicant]
C. Chamberland and E. T. Campbell, “A circuit-level protocol and analysis for twist-based lattice surgery,” arXiv e-prints (2022), 2201.05678 [quant-ph], pp. 1-12. [cited by applicant]