search

overshiki / SymbolicCircuit.jl

Symbolic system for Qauntum computing, using term rewriting & equality saturation technique to manipulate quantum circuit
MIT License
8 stars 1 forks source link

areequal may fail for longer circuit, due to timeout or out of eclasslimit during egraph saturation process #1

Open overshiki opened 2 years ago

overshiki commented 2 years ago 
using SymbolicCircuit

x1 = Gate(gX(), [Loc(1), ])
y3 = Gate(gY(), [Loc(3), ])
z2 = Gate(gZ(), [Loc(2), ])
z3 = Gate(gZ(), [Loc(3), ])
h2 = Gate(gH(), [Loc(2), ])
cnot_4c2 = Gate(gX(), [Loc(1), cLoc(2)])
rx1 = Gate(rX([:theta1, ]), [Loc(3), ])
rx2 = Gate(rX([:theta2, ]), [Loc(3), ])
s3 = Gate(gS(), [Loc(3), ])

circ = x1 * z2 * cnot_4c2 * z2 * y3 * z3 * x1 * s3 * s3 * rx1 * rx2 * h2
ncirc = egraph_simplify(circ, Val(:default_rule))
@show ncirc
@show SymbolicCircuit.areequal(Val(:default_rule), circ, ncirc)

This piece of code will return :timeout tag, if given longer time, it will return :eclasslimit tag. If given longer time and larger eclasslimit, it will be killed during running. This is an issue related to intrinsic time&memory complexity of algorithms related to egraph. And need more research work