6 ms·
I wonder how long it will be before state-of-the-art SAT solvers start incorporating similar networks.
by eutectic 10y ago
I wonder how long it will be before state-of-the-art SAT solvers start incorporating similar networks.
- letitgo12345 10y agoI 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.
- deepnotderp 10y agoIirc graph ConvNets have been successfully applied to some Boolean Sat problems.
- letitgo12345 10y agoOnly 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.
- CJefferson 10y agoHaving tried this myself, so far it doesn't work. The main problem is that SAT problems come in many different sizes, and while resampling a picture "makes sense" to make it smaller, resampling a SAT problem does not. Also the general lack of shape or structure makes things hard. NN can help bad SAT solvers get better, but the heuristics in the best ones are (at present) better than anything a NN can produce.