Multi-armed Bandit Algorithms for the Boolean Satisfiability Problem: A Survey

Abstract

This paper provides a survey of recent literature on the use of multi-armed bandit algorithms to solve the Boolean satisfiability problem (SAT), a well-known NP-complete problem with broad applications in academia and industry. The application of bandit algorithms in modern SAT solvers has achieved great success in recent years, as evidenced by the excellent performance of SAT solvers using bandit algorithms in SAT competitions. Bandit algorithms are classic randomized optimization algorithms that strike a balance between exploration and exploitation and can aid in designing and improving heuristics in SAT solvers. In this paper, we introduce several aspects of the application of bandit algorithms in modern SAT solvers, ranging from heuristic methods in CDCL and SLS solvers to strategies in parallel SAT solvers. The use of bandit algorithms in SAT solvers still holds great potential. In conclusion of the survey, we summarize the current issues and suggest possible future research directions.