about
Machine Learning Methods in Solving the Boolean Satisfiability Problem (arxiv.org)
2 points by wslh on Jul 9, 2023 | hide | past | pdf | discuss on HN

In plain words: It surveys recent attempts to solve the yes/no logic puzzle SAT with machine learning, from simple classifiers to fully learned solvers and hybrids with classic search solvers. Learning can replace hand-designed rules, but the review finds the field promising yet still limited and hard.

Abstract

This paper reviews the recent literature on solving the Boolean satisfiability problem (SAT), an archetypal NP-complete problem, with the help of machine learning techniques. Despite the great success of modern SAT solvers to solve large industrial instances, the design of handcrafted heuristics is time-consuming and empirical. Under the circumstances, the flexible and expressive machine learning methods provide a proper alternative to solve this long-standing problem. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT, as well as recent progress on combinations of existing CDCL and local search solvers with machine learning methods. Overall, solving SAT with machine learning is a promising yet challenging research topic. We conclude the limitations of current works and suggest possible future directions.

Wenxuan Guo, Junchi Yan, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, Yaohui Jin
arXiv:2203.04755 · cs.AI, cs.LG, cs.LO · submitted Mar 2, 2022
abstract · pdf · html

add comment on HN