4 ms·
Constraint solvers are a cool bit of magic. The article underplays how hard it is to model problems for them, but when you do have a problem that you can shape
by sophacles 1y ago
Constraint solvers are a cool bit of magic. The article underplays how hard it is to model problems for them, but when you do have a problem that you can shape into a sat problem... it feels like cheating.
- pkoird 1y agoGoing one abstraction deeper, SAT solvers are black magic.
- metadat 1y agoYes, 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.
- metadat 1y ago* s/happens/fades/
- mikestorrent 1y agoIf 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.
- mzl 1y agoHas there been any published example of where this solver outperforms a classical solver?
- ngruhn 1y agoI 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...
- almostgotcaught 1y agoThe solution is to look at a lot of examples https://www.hakank.org/ https://www.hakank.org/