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?