Hacker News Reader

The solution is to look at a lot of examples

https://www.hakank.org/

I took a course on SMT solvers in uni. It's so cool! They're densely packed with all these diverse and clever algorithms. And there is still this classic engineering aspect: how to wire everything up, make it modular...

If you're good at doing this, you should check out the D-Wave constrained quadratic model solvers - very exciting stuff in terms of the quality of solution it can get in a very short runtime on big problems.

Has there been any published example of where this solver outperforms a classical solver?

Going one abstraction deeper, SAT solvers are black magic.

Yes, explaining the "why / how did the SAT solver produce this answer?" can be more challenging than explaining some machine learning model outputs.

You can literally watch as the excitement and faith of the execs happens when the issue of explainability arises, as blaming the solver is not sufficient to save their own hides. I've seen it hit a dead end at multiple $bigcos this way.

* s/happens/fades/