I've been reading and learning about SAT solvers this week. If they can solve problems with thousands of variable quickly haven't we practically solved ANY problem that can be reduced to it, including the TSP problem? Or does it only work quickly for special cases?
2
-
8$\begingroup$ They don't work well for every instance of a problem. For example, AFAIK solvers fail on random SAT formulas with clauses-to-variables ratio close to the satisfiability threshold. The same should be true for SAT instances reduced from some cryptographic primitive, like factoring random large semiprimes. There is work on solving large TSP instances, but with specialized techniques, rather than SAT solvers. This talk by Bill Cook may be fun for you youtube.com/watch?v=q8nQTNvCrjE&t=35s $\endgroup$– Sasho NikolovDec 19, 2018 at 17:49
-
1$\begingroup$ Related / probably of interest to the OQ: cstheory.stackexchange.com/q/37886/129 $\endgroup$– Joshua GrochowDec 19, 2018 at 23:36
Add a comment
|