I think reducing the TSP to a SAT problem is not a very efficient approach. MIP solvers have become extremely sofisticated (and implement many of the techniques of SAT and much more) and offer a much more powerful modeling paradigm. it's hard to imagine a SAT solver outperforming them on such problems.