Comment by CJefferson | Hacker News Reader

Comment by CJefferson | Hacker News Reader

Parent Full thread

Surprisingly, for many problems (including travelling salesman), Sat solvers are very competitive. I research in this area and it is a constant source of annoyance when you come up with a clever special algorithm which then gets beaten by translation to SAT.

SAT particularly exceeds when you have side constraints. Imagine travelling salesman where you have to top up petrol only in cities, or where you need to sleep at night, or some roads are slower at rush hour, or you have a particular place you want to be at a particular time/date.

A specialised travelling salesman solver would be useless for any of these. Adding side constraints to SAT is simple.

In general, I wouldn't try to write sat models directly unless you are writing a logic problem. Consider looking at conjure ( https://github.com/conjure-cp/conjure ) which adds a nice language on top, and get target various NP complete solvers, including Sat (which often is the best). (I'm one of the minor conjure developers)

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?

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.

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

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.

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:

https://developers.google.com/optimization/

Reply on news.ycombinator.com