Cyclic circuit produced during Badger optimisation

[aborgna-q]

#200 is now fixed, but more bugs remain...

Edit: See Luca's clearer explanation below: #239 (comment)

Translating this qasm file into a hugr and applying the badger optimisation generates a cyclic graph. (Which causes the hashing code to panic).

OPENQASM 2.0;
include "qelib1.inc";

qreg q[5];
cx q[4],q[1];
cx q[3],q[4];
cx q[1],q[2];
cx q[4],q[0];
u3(0.5*pi,0.0*pi,0.5*pi) q[1];
cx q[0],q[2];
cx q[3],q[1];
cx q[0],q[2];

The failing example is here:
https://github.com/CQCL/tket2/blob/9f752895c649d6e22f6f190efe77d1187046b7c6/tket2/examples/non_dag.rs

Checkout debug/non-dag-example and cargo run --features portmatching --example non_dag.

[aborgna-q]

The problem comes from an erroneous invalidation set definition for the rewrite composition.

It's simpler to see it in this simpler (failing) circuits:

OPENQASM 2.0;
include "qelib1.inc";

qreg q[4];
cx q[0],q[1]; # a
cx q[2],q[3]; # b
h q[1];
h q[3];
cx q[2],q[1]; # c
cx q[0],q[3]; # d
h q[0];
h q[1];
h q[2];
h q[3];

(hadamards added for padding, so the immediate neighbours do not overlap).

In that circuit, two possible rewrites are:

• swap a and d
• swap b and c

On their own these are valid CNOT swaps.

But if both are applied simultaneously, they create a loop in the circuit.

Original circuit:

After swapping b and c:

After swapping a and d:

(Notice the loop in nodes $7 \to 3 \to 6 \to 13 \to 14 \to 4 \to 7$)

[lmondada]

Just a restatement that made it clearer for me, at the risk of being obvious to everyone already.

Swapping the two CX on qubit 0 gives you

q_0: ──■────■───────                         ───────■────■───────
     ┌─┴─┐  │  ┌───┐                                │  ┌─┴─┐┌───┐
q_1: ┤ X ├──┼──┤ X ├           ===>          ───────┼──┤ X ├┤ X ├
     └───┘  │  └─┬─┘                                │  └───┘└─┬─┘
q_2: ──■────┼────■──                         ──■────┼─────────■──
     ┌─┴─┐┌─┴─┐                              ┌─┴─┐┌─┴─┐     
q_3: ┤ X ├┤ X ├─────                         ┤ X ├┤ X ├──────────
     └───┘└───┘                              └───┘└───┘

And now the two CX not on qubit 0 (b and c) no longer form a convex pattern 🧐

[lmondada]

This could be resolved by introducing the concept of "convex set of (convex) patterns". Checking that a set of patterns is convex is quite similar to how we are checking convexity at the moment, and we could (presumably) reuse the precomputed convex checker data structure that we are already using.

Convex set of patterns: For every pair of patterns $P_1$, $P_2$ in the set, there are no nodes $b_1, a_1 \in P_1$ and $b_2, a_2 \in P_2$ such that $b_1$ is in the past of $a_2$ and $b_2$ is in the past of $a_1$. In other words: all nodes in $P_1$ are either in the past or spacelike-separated from all nodes in $P_2$, or they are all in the future or spacelike-separated.

This checking isn't free, unfortunately:

• for two patterns with $q$ qubits ($q$ is always small), you could check whether the $q$ smallest of $P_1$ are in the past of the $q$ largest in $P_2$ XOR whether the $q$ largest of $P_1$ are in the future of the $q$ smallest of $P_2$. For a set of $n$ patterns, this would take time $q^2 \cdot n^2$. The $n^2$ here will be expensive :/
• Enumerate patterns in a topsort order (this would be a simple and rather cheap change to make) and require conservatively that you can only add patterns to a set of patterns if it is in the future or spacelike-separated from any pattern in the set. This can be checked cheap-ish-ly by keeping an array of the $Q$ largest vertices (the largest vertex for each qubit) of the patterns already in the set, where $Q$ is the total number of qubits in the input (may be large). Then for each of the $q$ qubits in the pattern, check that the smallest in the pattern is larger than the one in the stored array. Worst case this would take time $\sim Q \cdot n$ (might be possible to make this faster), but at the cost of missing some valid sets of patterns. And it might still be too slow!

On top of this checking not being free, there is the argument that we should only check this once it's been filtered and is actually about to be applied, instead of computing this for sets that might well be discarded later on.

EDIT: this might require to precompute slightly different stuff than what we are doing now, but shouldn't be too far off.

[lmondada]

I'm not convinced any of what I'm saying is useful for a quick fix... Maybe we should turn this into a github discussion.

[aborgna-q]

Nice! Yes, I'm worried about the exploding complexity.
Let's move your comment to a discussion, and I'll implement a quick-but-not-optimal fix in the meantime.

Edit: #242