[UncleMeat]

SAT is NP-Complete. In principle, this means that SAT solvers don't scale. If we stopped here then we would never have developed symbolic execution. It turns out that SAT and SMT solvers do scale for lots of real world inputs. Cook's proof is amazingly elegant and powerful but fails to inform real development.

[tikhonj]

SAT solvers only scale sometimes. Complexity theory is a starting point for understanding why this "sometimes" is inevitable, but it never even implies that NP-complete problems are never tractable. Complexity theory gives us an understanding of how powerful and expressive SAT is which very much does inform real development.

Arguing that "SAT is NP-complete and therefore useless" is not misusing complexity theory, it's misunderstanding complexity theory—not misunderstanding some deep result or non-trivial consequence of complexity theory, but misunderstanding the fundamentals that are covered in the first lecture of the first class on the topic.

[bonoboTP]

It's common. My lecturer in the first lecture gave a motivation why we learn about this saying:imagine your boss proposes you compute <whatever>, then you - informed by this lecture - will recognize it belongs to an infeasible complexity class and can tell your boss it won't be possible.

We did learn the definitions but "worst case" was never highlighted as such, it was naturally assumed. The closest we got was the discussion that constant factors may matter for small problems and O analysis masks those differences.

[dllthomas]

> tell your boss it won't be possible

I mean, if your boss is demanding a solution that's both accurate and fast on every input, you can tell your boss that showing P=NP is probably out of scope of your project. But that's the start of a discussion about how to step back from that ideal, not the end of a discussion about the potential product.