alaarman / taiwan-2024

1 stars 0 forks source link

SMT Encoding #1

Open JingyiMei98 opened 3 months ago

JingyiMei98 commented 3 months ago

State

(S,G) → S*(sqrt(2))+ G We store a real number in a 2-tuple S: Bool^2n → Real

G: Bool^2n → Real

H_i:

forall x1,x2,…xn,z1,z2…zn : S’ (x1,…,xn,z1,…,zn) = ite(xi /\ zi, -1, 1) * S(x1,…,zi,…,xn,z1,..,xi…zn)

forall x1,x2,…xn,z1,z2…zn : G’ (x1,…,xn,z1,…,zn) = ite(xi /\ zi, -1, 1) * G(x1,…,zi,…,xn,z1,..,xi…zn)

S_i:

forall x1,x2,…xn,z1,z2…zn : S’ (x1,…,xn,z1,…,zn) = ite(xi /\ zi, -1, 1) * S(x1,…,xn,z1,..,xi XOR zi, …zn)

forall x1,x2,…xn,z1,z2…zn : G’ (x1,…,xn,z1,…,zn) = ite(xi /\ zi, -1, 1) * G(x1,…,xn,z1,..,xi XOR zi, …zn)

H_iS_i

S’ (x1,…,xn,z1,…,zn) = ite(xi /\ zi, -1, 1) * S(x1,…,zi,…,xn,z1,..,xi…zn) /\

S’’ (x1,…,xn,z1,…,zn) = ite(xi /\ zi, -1, 1) * S’(x1,…,xn,z1,..,xi XOR zi, …zn) /\

!S’’ (verification condition, which I don't know how yet…)

CX_i_j

bitwise XOR the ith column of the X matrix into the jth column of X matrix

bitwise XOR the jth column of the Z matrix into the ith column of Z matrix

forall x1,x2,…xn,z1,z2…zn : S’ (x1,…,xn,z1,…,zn) = ite(xi /\ zj /\ (xj XOR !zi), -1, 1) * S(x1,…,xi,…,xj XOR xi,…,xn,z1,..,zi XOR zj,…,zj,…zn)

forall x1,x2,…xn,z1,z2…zn : G’ (x1,…,xn,z1,…,zn) = ite(xi /\ zj /\ (xj XOR !zi), -1, 1) * G(x1,…,xi,…,xj XOR xi,…,xn,z1,..,zi XOR zj,…,zj,…zn)

T_i:

forall x1,x2,…xn,z1,z2…zn :

S’ (x1,…,xn,z1,…,zn) = ite(xi,1,0)(S(x1,…,xn,z1,…,zi==False,..zn)+ite(zi,1,-1)G(x1,…,xn,z1,…,zi==True,…,zn))+ ite(xi,0,1)*S(x1,…,xn,z1,…,zn)

G’(x1,…,xn,z1,…,zn) = ite(xi,1,0)(0.5)(S(x1,…,xn,z1,…,zi==False,…,zn) + ite(zi,1,-1)S(x1,…,xn,z1,…,zi==True,…,zn))+ ite(xi,0,1)G(x1,…xn,z1,…zn)

X → (X+Y)/2^0.5 Z→ Z Y → (Y-X)/2^0.5

S x1 z0 S’ → S x1 z1 S’ S x1 z0 S’ S x1 z1 S’ → S x1 z1 S’. -S x1 z0 S’

forall x1,x2,…xn,z1,z2…zn :

S’ (x1,…, xi=1,..,xn,z1,…, zi=1,..,zn) =

S (x1,…, xi=1,..,xn,z1,…, zi=0,..,zn)/2^0.5 + S(x1,…, xi=1 ,..,xn,z1,…, zi=1 ,..,zn)/2^0.5

S’ (x1,…, xi=1,..,xn,z1,…, zi=0,..,zn) =

S (x1,…, xi=1,..,xn,z1,…, zi=0,..,zn)/2^0.5 - S(x1,…, xi=1 ,..,xn,z1,…, zi=1 ,..,zn)/2^0.5

S’ (x1,…, xi=0,..,xn,z1,…, zi=1,..,zn) =

S (x1,…, xi=0,..,xn,z1,…, zi=1,..,zn)

S’ (x1,…, xi=0,..,xn,z1,…, zi=0..,zn) =

S (x1,…, xi=0,..,xn,z1,…, zi=0,..,zn)

S’(XZ) = (1/2^0.5) ^ ite(~X /\ ~Z, 0, 1) S(XZ) + (1/2^0.5) ^ ite(X xor Z, 0, 1) S(X\bar{Z})

============================

Use Array

S’ = store (S, i, j)

forall x, S’(x) = ite(i=x , j, S(x) )

JingyiMei98 commented 3 months ago

Let f(xz) be the coefficients for Pauli matrices \sigma[xz] for the input state, i.e. rho1 = f(00) I + f(01) Z + f(10) X + f(11) Y, and g(xz) be the coefficients for the state rho2 = T rho1 T^dagger, i.e. rho2 = g(00) I + g(01) Z + g(10) X + g(11) Y, we have: g(00) = f(00) g(10) = 1/sqrt(2) f(10) – 1/sqrt(2) f(11) g(01) = f(01) g(11) = 1/sqrt(2) f(10) + 1/sqrt(2) f(11)

g(x,z) = ite(x, 1/sqrt(2)( f(1,0) + ite(z, -f(11), f(11)) ), f(x,z)), where ite(x, s1, s2) means if x is True then s1, else s2.

For Clifford + T circuits, the coefficients of all possible output states are in the form of a sqrt(2) + b, where a and b are rational numbers. Thus the coefficients f(xz) can be exactly encoded as a pair, i.e. f(xz) = (a, b). Moreover, since 1/ sqrt(2) (a sqrt(2) + b) = (b/2) sqrt(2) + a, we have 1/ sqrt(2) f(xz) = (b/2, a)