5 ms·
Traveling salesmen is even solved to optimality (no heuristics) for pretty large instances with integer programming techniques. Also SAT is pretty much a solve
by ngruhn 3y ago
Traveling salesmen is even solved to optimality (no heuristics) for pretty large instances with integer programming techniques.
Also SAT is pretty much a solved problem. With algorithms like CDCL.
This really surprised me. I also left my first complexity theory course believing that NP-hard = "not solvable in practice“
- fooker 3y ago> SAT is pretty much a solved problem We don’t really understand what makes some SAT problems harder than others. You can go from a problem solvable with CDCL in a few seconds to one that would outlast the solar system by changing a couple of input bits.
- ngruhn 3y agoSure, but in practice that’s not what people worry about, from what I have seen. At least when dealing with SMT problems, the SAT part is the easy part.
- empath-nirvana 3y agoI think that's because _in practice_ people don't waste their time working on intractable problems if they just want to get something done. There's almost always some way to avoid the intractable problem and approach it a different way. It's sort of like how "in practice" it didn't matter for thousands of years that nobody understood electricity. Any problem that came up that would have required that knowledge to solve just got dropped, because they didn't have the tools to solve it.
- Legend2440 3y agoIt's always about worst-case complexity; you may be able to solve typical problems much easier. This even applies to the halting problem, which is unsolvable in general but pretty easy for most real programs. But also, "pretty large" is relative. Wikipedia says the largest known exact solution for a traveling salesman problem is 85,900 nodes, which is not really that many.