nice!
can you show a quick scalability graph (e.g. does this work for mapping a 20q circuit or does it blow up)

With our benchmarks? Sure.. let me try.

With our benchmarks? Sure.. let me try.

or just any random circuit.

Also... There are a couple other projects in the pipeline that use Z3. Can you use that instead? It's probably faster than python-constraints

So I am guessing that this is in essence finding if there is a sub-graph of the device topology in which the circuit fits exactly. That would make it equivalent to the sub-graph isomorphism problem that is NP-Complete.

Yes this is a satisfiability problem and should be exponential in the number of constraints, but I would like to put some numbers to the overheads so we can decide on a cutoff to use this pass vs. switching to a more scalable pass.

I tried with

cmap20 = CouplingMap(FakeTokyo().configuration().coupling_map)
nqubits = [4, 8, 12, 16, 20]
depths = [16, 32, 64, 128, 256, 512, 1024, 2048, 4096]

for nqubit in nqubits:
    for depth in depths:
        circuit = random_circuit(nqubit, depth)
        dag = circuit_to_dag(circuit)
        pass_ = CSPLayout(cmap20)
        import time

        start = time.process_time()
        pass_.run(dag)
        print('nqubit:', nqubit, 'depth:', depth, time.process_time() - start)
        print('None' if pass_.property_set['layout'] is None else 'not None')

After nqubit: 4 depth: 4096 (it took 0.04 seconds), it cannot find any solution. The worst situation was less than half second. I think it can be a good attempt before applying TrivialLayout.

python-constraint is a simple pure python lib. Z3 is a full different animal. I can explore Z3 for more hard core options. But still think that this approach is very light-weight and it should be considered before TrivialLayout. At least for some optimization levels.

python-constraint is a simple pure python lib. Z3 is a full different animal. I can explore Z3 for more hard core options. But still think that this approach is very light-weight and it should be considered before TrivialLayout. At least for some optimization levels.

While I agree z3 will probably be faster I just took a look at what the packaging story is for z3 since it's a C++ library with a Python API and that can be problematic in some cases especially for lesser used libs.

It's not great besides not publishing releases to pypi match every project release https://pypi.org/project/z3-solver/#history vs https://github.com/Z3Prover/z3/releases (conda's in an even worse state: https://anaconda.org/asmeurer/z3/files the last release there was >3years ago). Then on the pypi side they don't publish osx wheels at all: https://pypi.org/project/z3-solver/#files which means we're making every mac user build it from source everytime we install qiskit. If we want to depend on z3 in the future, we'll probably have to work with them to improve their packaging.

If at some stage we want to go heavyweight with this, we have a couple of in-house of CSP and SAT engines at our disposal - though C++, none Python. One comment though - both CSP and SAT are supposed exponential in the number of variables, but linear in number of constraints - in fact adding constraints many times greatly reduce runtime to solution because it efficiently prunes the search tree. Also, in our case the challenge is optimization - not satisfaction per se, so may need to consider engines which deal efficiently with soft constraints hierarchies. The other option is to do a log-search with adding an upper-bound constraint after each run, but this is a constraint CSP engines don't deal with very well. Z3 has an interface to soft constraints, but I never checked to what extent it can actually deal with them

I haven't reviewed all the code in depth yet, but the release notes (which are great details thanks for writing them) are in the wrong format.

Ups! Fixed in b445b41