🐛 Incorrect stripping of idle qubits that are not idle in both circuits

burgholzer commented 5 months ago

Environment information

Any OS or Python version. Dates back to the very beginning of QCEC.

Description

If two circuits work on the same number of qubits and one of them has an idle qubit (a qubit that does not have a gate acting on it), the equivalence check might fail because the output permutations of the circuits might not match after the idle qubit in one circuit has been stripped.

This behavior is a result of the fact that the circuits are stripped of idle qubits in isolation, i.e., without considering the other circuit. https://github.com/cda-tum/mqt-qcec/blob/5d9cbc10421298abfdf4a52cfbed89de85f385c9/src/EquivalenceCheckingManager.cpp#L210-L212

Expected behavior

An idle qubit should only be removed if it either

is idle in both circuits
is idle in one and does not exist in the other circuit

This requires a dedicated stripIdleQubits method in QCEC that considers both circuits in conjunction. A corresponding implementation can be heavily inspired by the original mqt-core implementation. However, I believe that the overall logic could even be improved a little bit given the constrained setting here in QCEC.

How to Reproduce

TEST_F(EqualityTest, NotEqualBecauseOfIdleQubitStripping) {
  // we measure only the second qubit
  qc1 = qc::QuantumComputation(2, 1);
  qc1.h(0);
  qc1.x(1);
  qc1.measure(1, 0);
  qc1.setLogicalQubitGarbage(0);

  // the first qubit doesn't have gates here, so stripIdleQubits() will remove
  // it and change the output permutation accordingliy
  qc2 = qc::QuantumComputation(2, 1);
  qc2.x(1);
  qc2.measure(1, 0);
  qc2.setLogicalQubitGarbage(0);

  // run the construction checker -> it will result in `NotEquivalent` because
  // the two circuits have a different output permutation after `stripIdleQubits()`
  config.execution.runConstructionChecker = true;
  ec::EquivalenceCheckingManager ecm(qc1, qc2, config);
  ecm.run();
  EXPECT_EQ(ecm.equivalence(), ec::EquivalenceCriterion::NotEquivalent);
}

Thanks @reb-ddm for bringing this up!

clerusch commented 3 months ago

I think I am having a related issue: If I try to run the following circuit in its qecc variant: The ecc circuit associated with the second two qubits before the red circle looks like this, encoding only two qubits (17 physical): While encoding the circuit after the circle looks like this, encoding all 4 qubits (31 physical): It would therefore appear that the CNOT connection between the first two qubits circuit to the second two qubits circuit at the start is optimized away due to being empty controls. This is a problem, because while it might seem like CNOTs controlled from qf2.0 in the |0> state would be irrelevant, since they dont change the target qubit, they actually do affect the state in the control qubit qf2.0 if the target qubit is not in a Z eigenstate.

burgholzer commented 3 months ago

I think I am having a related issue: If I try to run the following circuit in its qecc variant: The ecc circuit associated with the second two qubits before the red circle looks like this, encoding only two qubits (17 physical): While encoding the circuit after the circle looks like this, encoding all 4 qubits (31 physical): It would therefore appear that the CNOT connection between the first two qubits circuit to the second two qubits circuit at the start is optimized away due to being empty controls. This is a problem, because while it might seem like CNOTs controlled from qf2.0 in the |0> state would be irrelevant, since they dont change the target qubit, they actually do affect the state in the control qubit qf2.0 if the target qubit is not in a Z eigenstate.

I am fairly sure this is not related to the issue above as QCEC does not optimize away these kinds of gates. As you say, they do influence the overall functionality. However, I am not quite confident that QCEC can even handle the two circuits you show here. First, its dynamic quantum circuit support is still rather experimental. Secondly, these circuits do not act on the same number of qubits; so I am not quite sure how the equivalence check would even work in that case conceptually.

Could you maybe provide some more information on your particular setting and maybe even the circuits you are trying to verify? Either QASM2 or Qiskit QPY or Qiskit Code to generate the circuits would work.

cda-tum / mqt-qcec