Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I doubt anytime soon (at least as part of current SAT solvers). A big barrier to applying ML to the process of SAT solving is that a lot of times, it's just faster to do a search with a simple heuristic for variable selection than try a much more time consuming ML method (and neural networks will be quite time consuming relative to the kinds of heuristics usually used) to do variable selection better.

Quantum is a special case really as DFT computation is already very time consuming.



Iirc graph ConvNets have been successfully applied to some Boolean Sat problems.


Only ones I've seen try and predict the satisfiability directly. But usually in SAT, you're either interested in a solution or a proof of infeasibility. Prediction can't do the latter and afaik, existing non-ML based SAT solvers are far better at doing the former.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: