Hacker News Reader

Comment by fweimer | Hacker News Reader

I know that historically, we were taught that NP-complete problems are unsolvable for interesting problem sizes, but that was already a bit of lie in when I went to university. (TSP was presented as a warning example, but even back then, very efficient approximations existed.)

These days, when you have a SAT-like problem, you're often done because you can throw a SAT solver at it, and it will give you an answer in a reasonable time. Particularly for such small problems like this one here. We routinely solve much larger and less structured SAT instances, e.g. when running package managers.

View on HN

> These days, when you have a SAT-like problem, you're often done because you can throw a SAT solver at it, and it will give you an answer in a reasonable time

I don't know. All my experiences with SAT solvers have been bad. Sometimes adding constraints (and making the problem overconstrained) makes them orders of magnitude faster, sometimes it makes them orders of magnitude slower. Same goes for changing variables from integer to real or vice versa. And it varies from SAT solver to SAT solver, even on the same problem. I know enough about SAT solvers to know why this might happen but they're complete black boxes (as far as I can tell) and I can't predict their performance at all nor can I predict if a change I attempt will make them behave better or worse. I can't even tell if the bad performance is my fault or just the problem being legitimately to hard. And when it works I'm never sure if it will always work or if there are some inputs we have that will slip through the cracks of the heuristics it's using and hit us with a running time measured in days. If I could never use a SAT solver ever again I wouldn't.

I know, my PhD was about verifying software correctness with SMT solvers.

The reason we don't do this in production is that the solvers take an unpredictable amount of time. A small problem can take forever and a large problem can be instant. You can't gave that in a compiler.

There are enough people at Apple who know about SAT solvers. :)

On the other hand, they might know about SAT solvers, but not have enough time to actually experiment with it and integrate one into the language. Especially if there are other high priority issues.

depends what you consider interesting and/or acceptable solution I suppose

Reply on news.ycombinator.com