<p>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?</p>

CC BY-SA 4.0
2018-12-19T17:49:49.987Z
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
CC BY-SA 4.0
2018-12-19T23:36:17.970Z
Related / probably of interest to the OQ: https://cstheory.stackexchange.com/q/37886/129
Joshua Grochow
<complexity>
SAT Solvers and their applications
Code_Newbie
# SAT Solvers and their applications

(Asked by: username_0 on 2018-12-19)

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?

**Tags:** complexity

> **Comments:**
> **username_1**: 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  
> **username_2**: Related / probably of interest to the OQ: https://cstheory.stackexchange.com/q/37886/129  

---

## 0 answers

