🐛 Endless execution of MQT QCEC's `verify` method

[jose]

System and Environment Information

• Apple M3 Max with MacOS v15.6.1 and Rocky Linux v8.5 (aarch64)
• MQT QCEC v3.1.0
• Python v3.13.1

Bug Description

What happened?

Given two specific quantum circuits, MQT QCEC's verify method runs endless and therefore does not report any result.

What did you expect to happen instead?

I would expect MQT QCEC's verify method to report that the two provided quantum circuits are either not_equivalent, equivalent, equivalent_up_to_global_phase, equivalent_up_to_phase, probably_equivalent, probably_not_equivalent, or no_information in case something went wrong.

Steps to Reproduce

Executing the following script:

import sys
from qiskit.qasm2 import load, LEGACY_CUSTOM_INSTRUCTIONS
from mqt.qcec import verify
from mqt.qcec.pyqcec import Configuration

# Load files
print("[DEBUG] Loading inputs...")
a = sys.argv[1]
b = sys.argv[2]
a_qc = load(filename=a, custom_instructions=LEGACY_CUSTOM_INSTRUCTIONS)
print(f"[INFO] {a_qc}")
b_qc = load(filename=b, custom_instructions=LEGACY_CUSTOM_INSTRUCTIONS)
print(f"[INFO] {a_qc}")

# Configure MTQ QCEC
print("[DEBUG] Configuring 'MTQ QCEC'...")
config = Configuration()
config.execution.run_construction_checker      = False
config.execution.run_alternating_checker       = True
config.execution.run_simulation_checker        = True
config.execution.run_zx_checker                = True
config.functionality.trace_threshold           = 1e-13
config.functionality.check_partial_equivalence = False
config.simulation.fidelity_threshold           = 1e-13

# Run verify
print("[DEBUG] Running 'verify'...")
v = verify(a_qc, b_qc, config)
print(f"[INFO] {v}")

as

python bug-issue-report.py <file> <file>

results in the following:

Command	Result
python bug-issue-report.py a.txt a.txt	equivalent (as expected)
python bug-issue-report.py b.txt b.txt	equivalent (as expected)
python bug-issue-report.py a.txt b.txt	unknown
python bug-issue-report.py b.txt a.txt	unknown

I ran the third and fourth command for an hour and MTQ QCEC's verify did not report result. I also tried both commands with a timeout of 60 seconds, i.e.,

config.execution.timeout = 60

but the execution never stopped. (This note could perhaps explain why.)

(You might find the quantum circuits a.txt and b.txt in here and here.)

[burgholzer]

Hey 👋🏼
Thanks for opening this issue and providing a reproducer.
I suspect that this has to do with one of the checker getting stuck and, as explained in the note that you found, there being no way to stop that runner.

Could you try the following and report back with your results?

• try with config.execution.parallel = False (this disables executing all checkers in parallel)
• in separate runs, only enable one of the checkers at a time, to understand which of the checkers is getting stuck.

My suspicion would be that it is the alternating checker and that it has to do with some numerical inaccuracies due to the structure of the circuits (small rotation angles).
Would be great if you could run the above tests. Happy to take a more detailed look afterwards.

[jose]

try with config.execution.parallel = False (this disables executing all checkers in parallel)

construction_checker	alternating_checker	simulation_checker	zx_checker	parallel	result
false	true	true	true	true	unknown
false	true	true	true	false	not_equivalent

in separate runs, only enable one of the checkers at a time, to understand which of the checkers is getting stuck.

construction_checker	alternating_checker	simulation_checker	zx_checker	parallel	result
false	false	false	false	true	no_information
true	false	false	false	true	unknown
false	true	false	false	true	unknown
false	false	true	false	true	not_equivalent
false	false	false	true	true	probably_not_equivalent

My suspicion would be that it is the alternating checker ...

It gets stuck in the construction checker and the alternating checker.

[burgholzer]

Thanks for checking! That essentially confirms my suspicion.
Since the circuits seem to be non-equivalent, the approaches that the alternating and the construction checker use cannot result in a compact intermediate data structure. And 2^17 x 2^17 just seems large enough for this to not finish in any reasonable time.

We really need to find a way to handle the parallelism in a better way.
I have an idea in mind about switching from multi-threading to multi-processing for the parallelism. While you cannot abort threads in C++ without waiting for completion, IIRC, processes can be killed.
I am not quite sure how fast I can get to this, but I hope that with the workarounds above you at least have a way to get results.