Quantum System: building automatic quantum compiler
Equivalent Circuit Classes (ECCs): a set of circuits that perform the same task
subsumed transformation: valid transformation
(n,q)-complete EECs: biggest EEC of certain function that has at most n gates and q qubits
Subcircuit: a collection of gates in a circuits that are executed in close neighborehood of computation graph. (If I execute subcircuit in appropriate time, it will never go wrong.)
Parametric gates: gates that needs input to define and construct. For a circuit with m parameters and q qubits, the circuit is written as:
Equivalence: |\psi\rangle and e^{i\beta}|\psi\rangle is equivalent up to a global phase. From an observational point of view, they are identical.
Circuit: C^{(n, q)}
fix gate set G
fixed parameter expression \Sigma
Representative Circuit: an arbitrary circuit that is one of the smallest in a EEC set in which the functionality is what we care about. // TODO: you should put definition of representation in front. and you didn't define "previous round" to have EECs instead of one EEC.
Circuit Transformation: a tuple (C_T, C_R) is a target and a rewrite. An EEC with x circuit has x(x-1) many transformations.
Fingerprint: randomly fix parameter p_0 and two quantum state, the finger print of a circuit is the following.
Pipeline: transformation generation and transformation applier
Generation:
start from representation with n gates
add one gate to representation, now with n+1 gates but with redundant (possibly different functionality, but we track them non-the-less)
eliminate redundant representation to get new n+1 representation
Applier:
circuit pruning
circuit optimizer: apply local transformation to the whole circuit based on cost before qubit mapping based on queue of cost using TASO. It applies transformation to some "almost-best" cost circuit (not seen before).
Performance: generation takes 30 min. Reduction gate count around 40%.
// QUESTION: why verifier?
// QUESTION: section related to phrase factor is unclear to me. Why SMT prover cannot prove Quartz
Given the number of qubits, we can prove a bound on how many CNOT to use at maximum. However, this bound isn't very useful if you don't assume full connectivity between all qubits. You can use SWAP (which uses 3 CNOT gate), but will be 4x~9x longer. Also, since physically you can't make your unitrary transform accurate, we just might as well evaluate the optimized algorithm by distance close to original matrix.
Since CNOT and U3 can represent all unitrary, we can transform the space of all possible CNOT and U3 combination into a tree space. We can do A on a tree space with some fitted heuristic function generated by brute force search. Brute force search for three qubit QFT takes one hour, while A takes only seven minutes.
Directions
physical level is not done
quartz: logical
mapping
physical
Question:
assumption on connectivity
assumption on logical gate set
assumption on actual gate set
Table of Content