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.

https://rise4fun.com/Z3/tutorialcontent/optimization