8

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?

Code_Newbie
  • 81
  • 1
  • 8
    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 https://www.youtube.com/watch?v=q8nQTNvCrjE&t=35s – Sasho Nikolov Dec 19 '18 at 17:49
  • 1
    Related / probably of interest to the OQ: https://cstheory.stackexchange.com/q/37886/129 – Joshua Grochow Dec 19 '18 at 23:36

0 Answers0