Finding clifford circuit solutions using SMT solvers

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.