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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.