search

System-Verification-Lab / Quokka-Sharp

2 stars 0 forks source link

The tool reports an incorrect answer `False` when checking two identical circuits. #35

Open alan23273850 opened 3 months ago

alan23273850 commented 3 months ago

The tool reports an incorrect answer False in the following example

~/Quokka-Sharp/experiment/benchmark/algorithm/origin$ ~/Quokka-Sharp/experiment/eq_run.py "~/GPMC/bin/gpmc -mode=1" grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm

with a running time of 71.26 seconds.

The two identical circuits should be equivalent, and the expected answer is True.

Did I do something wrong?

alan23273850 commented 3 months ago

I also figured out that the output becomes True if the gpmc mode is switched to 3

~/Quokka-Sharp/experiment/benchmark/algorithm/origin$ ~/Quokka-Sharp/experiment/eq_run.py "~/GPMC/bin/gpmc -mode=3" grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm

with a running time of 0.55 seconds.

Maybe it's the problem caused by gpmc.

alan23273850 commented 3 months ago

Besides, I would also like to know whether one can control the number of processes of gpmc at a time, because the number of cores on a server may not be enough. Thanks.

alan23273850 commented 3 months ago

But actually, there is also some inconsistency when the gpmc mode is switched to 3.

For instance, ~/AutoQ/equivalence_or_not/flip$ ~/Quokka-Sharp/experiment/eq_run.py "~/GPMC/bin/gpmc -mode=3" a.qasm b.qasm returns True (incorrect) with running time 0.47 seconds.

~/AutoQ/equivalence_or_not/flip$ ~/Quokka-Sharp/experiment/eq_run.py "~/GPMC/bin/gpmc -mode=1" a.qasm b.qasm returns False (correct) with running time 0.19 seconds.

and a.qasm and b.qasm are NOT equivalent.

a.qasm:

OPENQASM 2.0;
include "qelib1.inc";
qreg q[16];
rz(0) q[0];
rx(0.5*pi) q[0];
rz(3*pi/4) q[0];
rx(0.5*pi) q[0];
rz(3*pi) q[0];
rz(pi/2) q[0];
rx(0.5*pi) q[0];
rz(pi/2) q[0];
rz(0) q[1];
rx(0.5*pi) q[1];
rz(45607*pi/65536) q[1];
rx(0.5*pi) q[1];
rz(3*pi) q[1];
rz(pi/2) q[1];
rx(0.5*pi) q[1];
rz(pi/2) q[1];
rz(0) q[2];
rx(0.5*pi) q[2];
rz(43691*pi/65536) q[2];
rx(0.5*pi) q[2];
rz(3*pi) q[2];
rz(pi/2) q[2];
rx(0.5*pi) q[2];
rz(pi/2) q[2];
rz(0) q[3];
rx(0.5*pi) q[3];
rz(5305*pi/8192) q[3];
rx(0.5*pi) q[3];
rz(3*pi) q[3];
rz(pi/2) q[3];
rx(0.5*pi) q[3];
rz(pi/2) q[3];
rz(0) q[4];
rx(0.5*pi) q[4];
rz(41541*pi/65536) q[4];
rx(0.5*pi) q[4];
rz(3*pi) q[4];
rz(pi/2) q[4];
rx(0.5*pi) q[4];
rz(pi/2) q[4];
rz(0) q[5];
rx(0.5*pi) q[5];
rz(20427*pi/32768) q[5];
rx(0.5*pi) q[5];
rz(3*pi) q[5];
rz(pi/2) q[5];
rx(0.5*pi) q[5];
rz(pi/2) q[5];
rz(0) q[6];
rx(0.5*pi) q[6];
rz(20153*pi/32768) q[6];
rx(0.5*pi) q[6];
rz(3*pi) q[6];
rz(pi/2) q[6];
rx(0.5*pi) q[6];
rz(pi/2) q[6];
rz(0) q[7];
rx(0.5*pi) q[7];
rz(39857*pi/65536) q[7];
rx(0.5*pi) q[7];
rz(3*pi) q[7];
rz(pi/2) q[7];
rx(0.5*pi) q[7];
rz(pi/2) q[7];
rz(0) q[8];
rx(0.5*pi) q[8];
rz(4935*pi/8192) q[8];
rx(0.5*pi) q[8];
rz(3*pi) q[8];
rz(pi/2) q[8];
rx(0.5*pi) q[8];
rz(pi/2) q[8];
rz(0) q[9];
rx(0.5*pi) q[9];
rz(39157*pi/65536) q[9];
rx(0.5*pi) q[9];
rz(3*pi) q[9];
rz(pi/2) q[9];
rx(0.5*pi) q[9];
rz(pi/2) q[9];
rz(0) q[10];
rx(0.5*pi) q[10];
rz(38877*pi/65536) q[10];
rx(0.5*pi) q[10];
rz(3*pi) q[10];
rz(pi/2) q[10];
rx(0.5*pi) q[10];
rz(pi/2) q[10];
rz(0) q[11];
rx(0.5*pi) q[11];
rz(38631*pi/65536) q[11];
rx(0.5*pi) q[11];
rz(3*pi) q[11];
rz(pi/2) q[11];
rx(0.5*pi) q[11];
rz(pi/2) q[11];
rz(0) q[12];
rx(0.5*pi) q[12];
rz(9603*pi/16384) q[12];
rx(0.5*pi) q[12];
rz(3*pi) q[12];
rz(pi/2) q[12];
rx(0.5*pi) q[12];
rz(pi/2) q[12];
rz(0) q[13];
rx(0.5*pi) q[13];
rz(4777*pi/8192) q[13];
rx(0.5*pi) q[13];
rz(3*pi) q[13];
rz(pi/2) q[13];
rx(0.5*pi) q[13];
rz(pi/2) q[13];
rz(0) q[14];
rx(0.5*pi) q[14];
rz(38039*pi/65536) q[14];
rx(0.5*pi) q[14];
rz(3*pi) q[14];
rz(pi/2) q[14];
rx(0.5*pi) q[14];
rz(pi/2) q[14];
x q[15];
cx q[15],q[14];
rz(pi/2) q[14];
rx(0.5*pi) q[14];
rz(pi/2) q[14];
rz(0) q[14];
rx(0.5*pi) q[14];
rz(93033*pi/65536) q[14];
rx(0.5*pi) q[14];
rz(3*pi) q[14];
cx q[14],q[13];
rz(pi/2) q[13];
rx(0.5*pi) q[13];
rz(pi/2) q[13];
rz(0) q[13];
rx(0.5*pi) q[13];
rz(11607*pi/8192) q[13];
rx(0.5*pi) q[13];
rz(3*pi) q[13];
cx q[13],q[12];
rz(pi/2) q[12];
rx(0.5*pi) q[12];
rz(pi/2) q[12];
rz(0) q[12];
rx(0.5*pi) q[12];
rz(23165*pi/16384) q[12];
rx(0.5*pi) q[12];
rz(3*pi) q[12];
cx q[12],q[11];
rz(pi/2) q[11];
rx(0.5*pi) q[11];
rz(pi/2) q[11];
rz(0) q[11];
rx(0.5*pi) q[11];
rz(92441*pi/65536) q[11];
rx(0.5*pi) q[11];
rz(3*pi) q[11];
cx q[11],q[10];
rz(pi/2) q[10];
rx(0.5*pi) q[10];
rz(pi/2) q[10];
rz(0) q[10];
rx(0.5*pi) q[10];
rz(92195*pi/65536) q[10];
rx(0.5*pi) q[10];
rz(3*pi) q[10];
cx q[10],q[9];
cx q[14],q[15];
cx q[13],q[14];
cx q[12],q[13];
cx q[11],q[12];
cx q[10],q[11];
rz(pi/2) q[9];
rx(0.5*pi) q[9];
rz(pi/2) q[9];
rz(0) q[9];
rx(0.5*pi) q[9];
rz(91915*pi/65536) q[9];
rx(0.5*pi) q[9];
rz(3*pi) q[9];
cx q[9],q[8];
rz(pi/2) q[8];
rx(0.5*pi) q[8];
rz(pi/2) q[8];
rz(0) q[8];
rx(0.5*pi) q[8];
rz(11449*pi/8192) q[8];
rx(0.5*pi) q[8];
rz(3*pi) q[8];
cx q[8],q[7];
rz(pi/2) q[7];
rx(0.5*pi) q[7];
rz(pi/2) q[7];
rz(0) q[7];
rx(0.5*pi) q[7];
rz(91215*pi/65536) q[7];
rx(0.5*pi) q[7];
rz(3*pi) q[7];
cx q[7],q[6];
rz(pi/2) q[6];
rx(0.5*pi) q[6];
rz(pi/2) q[6];
rz(0) q[6];
rx(0.5*pi) q[6];
rz(45383*pi/32768) q[6];
rx(0.5*pi) q[6];
rz(3*pi) q[6];
cx q[6],q[5];
rz(pi/2) q[5];
rx(0.5*pi) q[5];
rz(pi/2) q[5];
rz(0) q[5];
rx(0.5*pi) q[5];
rz(45109*pi/32768) q[5];
rx(0.5*pi) q[5];
rz(3*pi) q[5];
cx q[5],q[4];
rz(pi/2) q[4];
rx(0.5*pi) q[4];
rz(pi/2) q[4];
rz(0) q[4];
rx(0.5*pi) q[4];
rz(89531*pi/65536) q[4];
rx(0.5*pi) q[4];
rz(3*pi) q[4];
cx q[3], q[4];
rz(pi/2) q[3];
rx(0.5*pi) q[3];
rz(pi/2) q[3];
rz(0) q[3];
rx(0.5*pi) q[3];
rz(11079*pi/8192) q[3];
rx(0.5*pi) q[3];
rz(3*pi) q[3];
cx q[3],q[2];
rz(pi/2) q[2];
rx(0.5*pi) q[2];
rz(pi/2) q[2];
rz(0) q[2];
rx(0.5*pi) q[2];
rz(87381*pi/65536) q[2];
rx(0.5*pi) q[2];
rz(3*pi) q[2];
cx q[2],q[1];
rz(pi/2) q[1];
rx(0.5*pi) q[1];
rz(pi/2) q[1];
rz(0) q[1];
rx(0.5*pi) q[1];
rz(85465*pi/65536) q[1];
rx(0.5*pi) q[1];
rz(3*pi) q[1];
cx q[1],q[0];
rz(pi/2) q[0];
rx(0.5*pi) q[0];
rz(pi/2) q[0];
rz(0) q[0];
rx(0.5*pi) q[0];
rz(5*pi/4) q[0];
rx(0.5*pi) q[0];
rz(3*pi) q[0];
cx q[9],q[10];
cx q[8],q[9];
cx q[7],q[8];
cx q[6],q[7];
cx q[5],q[6];
cx q[4],q[5];
cx q[3],q[4];
cx q[2],q[3];
cx q[1],q[2];
cx q[0],q[1];

b.qasm

// Used Gate Set: ['rz', 'sx', 'x', 'cx', 'measure']
OPENQASM 2.0;
include "qelib1.inc";
qreg q[16];

rz(0) q[0];
rx(0.5*pi) q[0];
rz(3*pi/4) q[0];
rx(0.5*pi) q[0];
rz(3*pi) q[0];
rz(pi/2) q[0];
rx(0.5*pi) q[0];
rz(pi/2) q[0];
rz(0) q[1];
rx(0.5*pi) q[1];
rz(45607*pi/65536) q[1];
rx(0.5*pi) q[1];
rz(3*pi) q[1];
rz(pi/2) q[1];
rx(0.5*pi) q[1];
rz(pi/2) q[1];
rz(0) q[2];
rx(0.5*pi) q[2];
rz(43691*pi/65536) q[2];
rx(0.5*pi) q[2];
rz(3*pi) q[2];
rz(pi/2) q[2];
rx(0.5*pi) q[2];
rz(pi/2) q[2];
rz(0) q[3];
rx(0.5*pi) q[3];
rz(5305*pi/8192) q[3];
rx(0.5*pi) q[3];
rz(3*pi) q[3];
rz(pi/2) q[3];
rx(0.5*pi) q[3];
rz(pi/2) q[3];
rz(0) q[4];
rx(0.5*pi) q[4];
rz(41541*pi/65536) q[4];
rx(0.5*pi) q[4];
rz(3*pi) q[4];
rz(pi/2) q[4];
rx(0.5*pi) q[4];
rz(pi/2) q[4];
rz(0) q[5];
rx(0.5*pi) q[5];
rz(20427*pi/32768) q[5];
rx(0.5*pi) q[5];
rz(3*pi) q[5];
rz(pi/2) q[5];
rx(0.5*pi) q[5];
rz(pi/2) q[5];
rz(0) q[6];
rx(0.5*pi) q[6];
rz(20153*pi/32768) q[6];
rx(0.5*pi) q[6];
rz(3*pi) q[6];
rz(pi/2) q[6];
rx(0.5*pi) q[6];
rz(pi/2) q[6];
rz(0) q[7];
rx(0.5*pi) q[7];
rz(39857*pi/65536) q[7];
rx(0.5*pi) q[7];
rz(3*pi) q[7];
rz(pi/2) q[7];
rx(0.5*pi) q[7];
rz(pi/2) q[7];
rz(0) q[8];
rx(0.5*pi) q[8];
rz(4935*pi/8192) q[8];
rx(0.5*pi) q[8];
rz(3*pi) q[8];
rz(pi/2) q[8];
rx(0.5*pi) q[8];
rz(pi/2) q[8];
rz(0) q[9];
rx(0.5*pi) q[9];
rz(39157*pi/65536) q[9];
rx(0.5*pi) q[9];
rz(3*pi) q[9];
rz(pi/2) q[9];
rx(0.5*pi) q[9];
rz(pi/2) q[9];
rz(0) q[10];
rx(0.5*pi) q[10];
rz(38877*pi/65536) q[10];
rx(0.5*pi) q[10];
rz(3*pi) q[10];
rz(pi/2) q[10];
rx(0.5*pi) q[10];
rz(pi/2) q[10];
rz(0) q[11];
rx(0.5*pi) q[11];
rz(38631*pi/65536) q[11];
rx(0.5*pi) q[11];
rz(3*pi) q[11];
rz(pi/2) q[11];
rx(0.5*pi) q[11];
rz(pi/2) q[11];
rz(0) q[12];
rx(0.5*pi) q[12];
rz(9603*pi/16384) q[12];
rx(0.5*pi) q[12];
rz(3*pi) q[12];
rz(pi/2) q[12];
rx(0.5*pi) q[12];
rz(pi/2) q[12];
rz(0) q[13];
rx(0.5*pi) q[13];
rz(4777*pi/8192) q[13];
rx(0.5*pi) q[13];
rz(3*pi) q[13];
rz(pi/2) q[13];
rx(0.5*pi) q[13];
rz(pi/2) q[13];
rz(0) q[14];
rx(0.5*pi) q[14];
rz(38039*pi/65536) q[14];
rx(0.5*pi) q[14];
rz(3*pi) q[14];
rz(pi/2) q[14];
rx(0.5*pi) q[14];
rz(pi/2) q[14];
x q[15];
cx q[15],q[14];
rz(pi/2) q[14];
rx(0.5*pi) q[14];
rz(pi/2) q[14];
rz(0) q[14];
rx(0.5*pi) q[14];
rz(93033*pi/65536) q[14];
rx(0.5*pi) q[14];
rz(3*pi) q[14];
cx q[14],q[13];
rz(pi/2) q[13];
rx(0.5*pi) q[13];
rz(pi/2) q[13];
rz(0) q[13];
rx(0.5*pi) q[13];
rz(11607*pi/8192) q[13];
rx(0.5*pi) q[13];
rz(3*pi) q[13];
cx q[13],q[12];
rz(pi/2) q[12];
rx(0.5*pi) q[12];
rz(pi/2) q[12];
rz(0) q[12];
rx(0.5*pi) q[12];
rz(23165*pi/16384) q[12];
rx(0.5*pi) q[12];
rz(3*pi) q[12];
cx q[12],q[11];
rz(pi/2) q[11];
rx(0.5*pi) q[11];
rz(pi/2) q[11];
rz(0) q[11];
rx(0.5*pi) q[11];
rz(92441*pi/65536) q[11];
rx(0.5*pi) q[11];
rz(3*pi) q[11];
cx q[11],q[10];
rz(pi/2) q[10];
rx(0.5*pi) q[10];
rz(pi/2) q[10];
rz(0) q[10];
rx(0.5*pi) q[10];
rz(92195*pi/65536) q[10];
rx(0.5*pi) q[10];
rz(3*pi) q[10];
cx q[10],q[9];
cx q[14],q[15];
cx q[13],q[14];
cx q[12],q[13];
cx q[11],q[12];
cx q[10],q[11];
rz(pi/2) q[9];
rx(0.5*pi) q[9];
rz(pi/2) q[9];
rz(0) q[9];
rx(0.5*pi) q[9];
rz(91915*pi/65536) q[9];
rx(0.5*pi) q[9];
rz(3*pi) q[9];
cx q[9],q[8];
rz(pi/2) q[8];
rx(0.5*pi) q[8];
rz(pi/2) q[8];
rz(0) q[8];
rx(0.5*pi) q[8];
rz(11449*pi/8192) q[8];
rx(0.5*pi) q[8];
rz(3*pi) q[8];
cx q[8],q[7];
rz(pi/2) q[7];
rx(0.5*pi) q[7];
rz(pi/2) q[7];
rz(0) q[7];
rx(0.5*pi) q[7];
rz(91215*pi/65536) q[7];
rx(0.5*pi) q[7];
rz(3*pi) q[7];
cx q[7],q[6];
rz(pi/2) q[6];
rx(0.5*pi) q[6];
rz(pi/2) q[6];
rz(0) q[6];
rx(0.5*pi) q[6];
rz(45383*pi/32768) q[6];
rx(0.5*pi) q[6];
rz(3*pi) q[6];
cx q[6],q[5];
rz(pi/2) q[5];
rx(0.5*pi) q[5];
rz(pi/2) q[5];
rz(0) q[5];
rx(0.5*pi) q[5];
rz(45109*pi/32768) q[5];
rx(0.5*pi) q[5];
rz(3*pi) q[5];
cx q[5],q[4];
rz(pi/2) q[4];
rx(0.5*pi) q[4];
rz(pi/2) q[4];
rz(0) q[4];
rx(0.5*pi) q[4];
rz(89531*pi/65536) q[4];
rx(0.5*pi) q[4];
rz(3*pi) q[4];
cx q[4],q[3];
rz(pi/2) q[3];
rx(0.5*pi) q[3];
rz(pi/2) q[3];
rz(0) q[3];
rx(0.5*pi) q[3];
rz(11079*pi/8192) q[3];
rx(0.5*pi) q[3];
rz(3*pi) q[3];
cx q[3],q[2];
rz(pi/2) q[2];
rx(0.5*pi) q[2];
rz(pi/2) q[2];
rz(0) q[2];
rx(0.5*pi) q[2];
rz(87381*pi/65536) q[2];
rx(0.5*pi) q[2];
rz(3*pi) q[2];
cx q[2],q[1];
rz(pi/2) q[1];
rx(0.5*pi) q[1];
rz(pi/2) q[1];
rz(0) q[1];
rx(0.5*pi) q[1];
rz(85465*pi/65536) q[1];
rx(0.5*pi) q[1];
rz(3*pi) q[1];
cx q[1],q[0];
rz(pi/2) q[0];
rx(0.5*pi) q[0];
rz(pi/2) q[0];
rz(0) q[0];
rx(0.5*pi) q[0];
rz(5*pi/4) q[0];
rx(0.5*pi) q[0];
rz(3*pi) q[0];
cx q[9],q[10];
cx q[8],q[9];
cx q[7],q[8];
cx q[6],q[7];
cx q[5],q[6];
cx q[4],q[5];
cx q[3],q[4];
cx q[2],q[3];
cx q[1],q[2];
cx q[0],q[1];
JingyiMei98 commented 3 months ago

I also figured out that the output becomes True if the gpmc mode is switched to 3

~/Quokka-Sharp/experiment/benchmark/algorithm/origin$ ~/Quokka-Sharp/experiment/eq_run.py "~/GPMC/bin/gpmc -mode=3" grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm

with a running time of 0.55 seconds.

Maybe it's the problem caused by gpmc.

Thanks for your interest in our tool!

In GPMC(https://git.trs.css.i.nagoya-u.ac.jp/k-hasimt/GPMC), the option mode is given as follows: -mode=\<0..3>

By setting mode=3, you are using projected weighted model counting. For example,

p cnf 3 4 c p show 2 3 0 c p weight 2 0.6 0 c p weight -2 0.4 0 -1 2 0 -2 3 0 2 -3 0 1 -2 3 0

only when you add all variables in 'c p show 2 3 0', it will be equal to weighted model counting (mode=1).

JingyiMei98 commented 3 months ago

Besides, I would also like to know whether one can control the number of processes of gpmc at a time, because the number of cores on a server may not be enough. Thanks.

Thanks for the suggestion! We will work on this and will let you know if this has been done.

JingyiMei98 commented 3 months ago

The tool reports an incorrect answer False in the following example

~/Quokka-Sharp/experiment/benchmark/algorithm/origin$ ~/Quokka-Sharp/experiment/eq_run.py "~/GPMC/bin/gpmc -mode=1" grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm grover-noancilla_nativegates_ibm_qiskit_opt0_5.qasm

with a running time of 71.26 seconds.

The two identical circuits should be equivalent, and the expected answer is True.

Did I do something wrong?

I assume the problem is caused by floating point error. We will look into this bug and get back to you as soon as possible.

alan23273850 commented 3 months ago

Okay, I see. So you mean in usual cases we should always set mode=1 and simply ignore all other settings.

BTW, I also believe your deduction about "floating point error," since the circuits we provide consist of gates of the form rx(a*pi/b) or rz(a*pi/b) with large denominators b. It is due to some reasons we need to convert your original circuits into such a form. This bug fix is recommended but not quite urgent. Thank you very much!