[ginko]

I have to admit that I haven't looked too closely into this but my understanding is that place & route is essentially an NP hard optimization problem. Would it be possible to translate this into a SAT problem and solve it with a state of the art SAT solver?

[kevmo314]

It's surely possible but if it's, for example, 10% slower, that easily eats into execution time and that directly translates into a sense of "maybe it's just worth it to pay the license fee for this year" after just a few 20h place and route runs.

Of course, if it were faster, that would be a huge win for the open source implementation.

[rowanG077]

Possible but the problem statement is generally way too large to throw into a SAT solver. You can do local problems with SAT though.