That's really interesting. But how does it actually work, in practice, to find an optimal TSP path given a SAT solver? I know there's a reduction proof, but if I remember correctly, the proof I learned involved transforming TSP from an optimization problem into a series of multiple decision problems of the form "Is there a path with length less than k?". That would mean running the SAT solver multiple times to get the right path length. Is that efficient enough, or is there a better way to do this?
It's more than just a SAT solver, but Microsoft's Z3 SMT solver has an option to minimize a quantity of interest. I haven't worked with it much, but it seemed faster than a binary search on 'k' when I was playing around with a non-TSP problem.
It usually is efficient enough, mainly because in practice it is very easy to find slightly too long paths, and fairly easy to prove smaller lengths unsatisfiable, so any solver spends most of its time proving, after finding the optimal value n, that n-1 isn't possible.
Some SAT solvers allow you to add additional constraints while they are running. So you can find a solution and then add additional constraints to try to get it to find a better one.
Something I found out, after participating in HashCode was that Google have a pretty comprehensive optimisation library called OR Tools. There is a module specifically for routing. I don't know what Google uses in production, but presumably this was developed for things like navigation:
