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?

  • 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$ Commented Dec 19, 2018 at 17:49
  • 1
    $\begingroup$ Related / probably of interest to the OQ: cstheory.stackexchange.com/q/37886/129 $\endgroup$ Commented Dec 19, 2018 at 23:36


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.