Concorde TSP is a solver for TSP. SAT solvers are solvers for boolean satisfiability. TSP and SAT are NP-complete.
Hence, why spent the time to develop Concorde TSP when there is an abundance of SAT solvers in the market back then?
$\begingroup$
$\endgroup$
0
Add a comment
|
$\begingroup$
$\endgroup$
1
TL;DR: polynomial reduction increases the size of a problem; using a specific solver allows you to exploit the structure of a problem.
When you reduce one NP-complete problem to another one, the size of the problem usually grows polynomially. For example, when you reduce a HAMPATH on a graph with $n$ nodes to SAT, the resulting formula has size of $\Theta(n^3)$ (I don't remember about the constant that arises in a straight-forward TSP->SAT reduction). If you use the Cook-Levin theorem, then the growth might be even bigger because a Turing machine might have really huge (polynomyal) overhead. NP-completeness is mostly a theoretical idea. So is a polynomial-time reduction. Many theoretical papers only state that there is a reduction, saying nothing about how practical it is.
Let's informally assume that TSP is as hard as SAT. It means that it takes similar computational resources to solve TSP on $n$ nodes and SAT with $n$ clauses if you use state-of-the-art solvers for each problem. Now it is easy to see that writing a separate solver is more practical than reducing the problem to SAT and using some existing SAT solver. It is all about polynomial overhead.
There is one more thing to notice: exact problems are usually simpler than broad ones. When you reduce TSP to SAT, the SAT solver knows nothing about the underlying structure of the formula. And special solvers for TSP, of course, deal with the fact that the input is a graph, the problem is to find a shortest Hamiltonian path, so on.
Although for some problems reduction to SAT can be reasonable, mostly if the problem is not well-studied (and no cool solvers exist) and when reduction doesn't increase the problem size a lot. SAT solvers are still very strong for many practical purposes.
-
1$\begingroup$ I think this is essentially the right answer. However, it is possible there is a reduction from a problem to another that only increases the size a little bit. Also, SAT solvers can be smart, and be able to detect structure especially if the encoding of the problem is suitable. Thus, it probably requires a bit of work to build a problem specific solver that beats a SAT solver. $\endgroup$ – Juho Oct 4 '16 at 8:14
