A Review of Research on Algorithms for Solving SAT Problems
DOI:
https://doi.org/10.54097/1mn6v127Keywords:
Exhaustive search; backtracking search; SAT solver algorithm; Conflict-Driven Learning Algorithms.Abstract
The SAT problem solving algorithms are an important research area in computer science aimed at solving the Boolean satisfiability problem. With the wide application of SAT problems in the fields of hardware design, automated planning, and artificial intelligence, researchers have proposed a variety of efficient solution algorithms. The classical algorithms include exhaustive search and backtracking search, but they are less efficient when dealing with large-scale problems. Heuristic search methods accelerate the search process by introducing randomization or evolutionary algorithms to improve the solution efficiency. Learning-based methods utilize learning and memorizing the explored search space or learning heuristic information to guide the search process. The CDCL algorithm, on the other hand, is an efficient conflict-driven learning algorithm that achieves impressive results by learning and applying conflict information to prune the search space. Parallel and distributed solving as well as quantum computing methods are hot research topics in recent years, which provide new ideas and technical support for solving large-scale problems. The research on algorithms for solving SAT problems continues to innovate, providing powerful tools and technical support for real-world problem solving.
References
Cook S. The complexity of theorem-proving procedures: Proceedings of the third annual ACM symposium on Theory of computing[C], 1971.
Davis M, Logemann G, Loveland D. A machine program for theorem-proving[J]. Journal of the ACM, 1962,5(7):394-397.
Selman B, Kautz H A, Cohen B. Local Search Strategies for Satisfiability Testing[J]. cliques coloring & satisfiability second dimacs implementation challenge, 1996.
Silva J P M, Sakallah K A. GRASP-A new search algorithm for satisfiability: Proceedings of International Conference on Computer Aided Design[C], San Jose, CA, USA, 1996.
Luby M, Sinclair A, Zuckerman D. Optimal speedup of Las Vegas algorithms[J]. Information Processing Letters, 1993,47(4):173-180.
Audemard G, Simon L. Predicting Learnt Clauses Quality in Modern SAT Solver: International Joint Conference on Artificial Intelligence[C], 2009.
Glover F, Kochenberger G, Hennig R, et al. Quantum bridge analytics I: a tutorial on formulating and using QUBO models[J]. Annals of Operations Research, 2022,314(1):141-183.
Reifenstein S, Leleu T, McKenna T, et al. Coherent SAT solvers: a tutorial[J]. Advances in Optics and Photonics, 2023,15(2):385-441.
Tiejun L, Kefan M, Jianmin Z. An Parallel FPGA SAT Solver Based on Multi-Thread and Pipeline[J]. Chinese Journal of Electronics, 2021,30(6):1008-1016.
Guo W, Zhen H, Li X, et al. Machine Learning Methods in Solving the Boolean Satisfiability Problem[J]. Machine Intelligence Research, 2023,20(5):640-655.
Jeroslow R G, Wang J. Solving propositional satisfiability problems[J]. Annals of Mathematics and Artificial Intelligence, 1990,1(1):167-187.
Kotelnikov V A, Kotelnikov M V. Use of the Bohm’s formula and its analogues in probe diagnostics[J]. High Temperature, 2017,55(4):477-480.
Freeman J W. Improvements to propositional satisfiability search algorithms[M]. University of PennsylvaniaComputer and Information Science Dept, 2000.
Moskewicz M W, Madigan C F, Zhao Y, et al. Chaff: engineering an efficient SAT solver: Proceedings of the 38th Design Automation Conference[C], Las Vegas, NV, USA, 2001.
H L J, V G, P P. Exponential recency weighted average branching heuristic for SAT solvers: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence[C], 2016.
Liang J H, V. K. H G, Poupart P, et al. An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate: Theory and Applications of Satisfiability Testing – SAT 2017[C], 2017.
Jin H, Somenzi F. Strong Conflict Analysis for Propositional Satisfiability: Proceedings of the Design Automation & Test in Europe Conference[C], Munich, Germany, 2006.
Hamadi Y, Jabbour S, Saïs L. What we can learn from conflicts in propositional satisfiability[J]. Annals of Operations Research, 2016,240(1):13-37.
Gomes C P, Selman B, Crato N, et al. Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems[J]. Journal of Automated Reasoning, 2000,24(1):67-100.
Biere A. PicoSAT Essentials.[J]. Journal on Satisfiability Boolean Modeling and Computation, 2008,2-4(4):75-97.
Luby M, Sinclair A, Zuckerman D. Optimal speedup of Las Vegas algorithms[J]. Information Processing Letters, 1993, 47(4):173-180.
M D, H P. A Computing Procedure for Quantification Theory [J]. Journal of the ACM, 1960,3(7):201-215.
Selman B, Levesque H, Mitchell D. A New Method for Solving Hard Satis ability Problems: In Proceedings of the tenth national conference on Artificial intelligence[C], 1992.
Kurin V, Godil S, Whiteson S, et al. Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver? Neural Information Processing Systems[C], 2020.
Ozolins E, Freivalds K, Draguns A, et al. Goal-Aware Neural SAT Solver[J]. International Joint Conference on Neural Networks, 2021:1-8.
Bünz B, Lamm M. Graph Neural Networks and Boolean Satisfiability[J]. arXiv preprint, 2017.
Balyo T, Sanders P, Sinz C. HordeSat: A Massively Parallel Portfolio SAT Solver: Theory and Applications of Satisfiability Testing[C], 2015.
Xu L, Hutter F, Hoos H H, et al. SATzilla: Portfolio-based Algorithm Selection for SAT[J]. Journal of Artificial Intelligence Research, 2008,32(1):565-606.
Downloads
Published
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
How to Cite
