This PR makes a rough attempt at adding a little interface for "constraint based addressing" schemes. Roughly speaking these are schemes where the problem of addressing a program is translated into some sort of constraint program (in this case, the language is SMT-LIB) which, if solved, can be used to back out the data required for addressing.
The only scheme implemented here is the TB-OLSQ (something like "transition based optimal layout synthesis for quantum computing") from Tan & Cong. What that paper does is to first define a scheme (OLSQ) that is truly worthy of the name "optimal" but which has very poor scaling properties (in terms of the number of variables / work done by a solver). The TB-OLSQ scheme is proposed as a modification of this in which gate placement and rewiring updates happen in alternating phases, handled in a way so that the complexity scales with the number of phases rather than with the number of gates or "time slices" (where perhaps two gates happen simultaneously). The quality of the output of this method seems to be within an additive constant (in term of # of swaps) of the costlier OLSQ method (I did a more substantial comparison of a few of these techniques a while back with an earlier Python implementation, but no longer have the results).
SMT-LIB and solvers can also be used to find constrained optima. In the case of TB-OLSQ, I give an optional :MINIMIZE-SWAPS argument to indicate that the total number of emitted swaps should be minimized. This could easily be adapted to allow for an infidelity cost (since we're not doing any nativizing, this just ends up being a sum over all swaps, but with swaps weighted by some constant associated with the link they are on). Note that finding a minimizer or maximizer is a lot slower than just finding some satisfying assignment for model parameters, so :MINIMIZE-SWAPS is off by default.
For the solver, we use cl-smt-lib which basically wraps a process running z3, exposing its i/o to Lisp in the form of a stream we can read from or write to. Because SMT-LIB has an s-expression syntax, it's pretty easy for us to just construct the constraint programs directly (but there is case sensitivty to deal with).
As it stands, this works in some test cases and I think can be useful for further experimentation, which is part of why I put it into its own system & package. There's basically no hook-up into the rest of the compiler, and so it's a bit of an island in that respect. There are two outstanding issues to work out before it could be incorporated more substantially into the "automatic" part of quilc:
The constraint-based schemes only handle "qubit allocation" or "gate placement". Nativization/logical synthesis/whatever you call it is assumed to have already been done. I think some thought would have to go into disentangling nativization from addressing to make these sort of schemes useful. But the possibility of such a 'disentangling' really depends on a homogenous view of hardware, which is perhaps still not reasonable (e.g. even if we can assume a common 2Q operator across all links on a chip, perhaps the fidelitiy varies substantially enough that we still want nativization and addressing combined).
Such schemes involve some magic parameters (for TB-OLSQ, the magic parameter is the number of phases or "blocks" to consider) and so some sort of search process for these. Solving or rejecting SMT-LIB programs can be very slow, and so we might want to incorporate some notion of a time budget into this search process if it's to be useable, particularly if we wish to do any kind of optimization (like :MINIMIZE-SWAPS).
This PR makes a rough attempt at adding a little interface for "constraint based addressing" schemes. Roughly speaking these are schemes where the problem of addressing a program is translated into some sort of constraint program (in this case, the language is SMT-LIB) which, if solved, can be used to back out the data required for addressing.
The only scheme implemented here is the TB-OLSQ (something like "transition based optimal layout synthesis for quantum computing") from Tan & Cong. What that paper does is to first define a scheme (OLSQ) that is truly worthy of the name "optimal" but which has very poor scaling properties (in terms of the number of variables / work done by a solver). The TB-OLSQ scheme is proposed as a modification of this in which gate placement and rewiring updates happen in alternating phases, handled in a way so that the complexity scales with the number of phases rather than with the number of gates or "time slices" (where perhaps two gates happen simultaneously). The quality of the output of this method seems to be within an additive constant (in term of # of swaps) of the costlier OLSQ method (I did a more substantial comparison of a few of these techniques a while back with an earlier Python implementation, but no longer have the results).
SMT-LIB and solvers can also be used to find constrained optima. In the case of TB-OLSQ, I give an optional
:MINIMIZE-SWAPSargument to indicate that the total number of emitted swaps should be minimized. This could easily be adapted to allow for an infidelity cost (since we're not doing any nativizing, this just ends up being a sum over all swaps, but with swaps weighted by some constant associated with the link they are on). Note that finding a minimizer or maximizer is a lot slower than just finding some satisfying assignment for model parameters, so:MINIMIZE-SWAPSis off by default.For the solver, we use
cl-smt-libwhich basically wraps a process runningz3, exposing its i/o to Lisp in the form of a stream we can read from or write to. Because SMT-LIB has an s-expression syntax, it's pretty easy for us to just construct the constraint programs directly (but there is case sensitivty to deal with).As it stands, this works in some test cases and I think can be useful for further experimentation, which is part of why I put it into its own system & package. There's basically no hook-up into the rest of the compiler, and so it's a bit of an island in that respect. There are two outstanding issues to work out before it could be incorporated more substantially into the "automatic" part of quilc:
The constraint-based schemes only handle "qubit allocation" or "gate placement". Nativization/logical synthesis/whatever you call it is assumed to have already been done. I think some thought would have to go into disentangling nativization from addressing to make these sort of schemes useful. But the possibility of such a 'disentangling' really depends on a homogenous view of hardware, which is perhaps still not reasonable (e.g. even if we can assume a common 2Q operator across all links on a chip, perhaps the fidelitiy varies substantially enough that we still want nativization and addressing combined).
Such schemes involve some magic parameters (for TB-OLSQ, the magic parameter is the number of phases or "blocks" to consider) and so some sort of search process for these. Solving or rejecting SMT-LIB programs can be very slow, and so we might want to incorporate some notion of a time budget into this search process if it's to be useable, particularly if we wish to do any kind of optimization (like
:MINIMIZE-SWAPS).