Progress in the Study of the Boolean Satisfiability Problem

Mengyu Guo

doi:10.62051/ijcsit.v2n2.25

Authors

Mengyu Guo

DOI:

https://doi.org/10.62051/ijcsit.v2n2.25

Keywords:

The Boolean satisfiability problem; NP Complete Problems; SAT solver algorithm; SAT Theory Foundation

Abstract

The Boolean Satisfiability problem (SAT) is a classical problem in computer science and artificial intelligence, and the most widely studied NP-complete problem. It aims to determine whether there exists an assignment of a value to a variable of a given Boolean formula that makes the formula true. In recent years, with the continuous improvement of theoretical research and practical application needs, the research on SAT problems has achieved remarkable results. These advances have not only promoted the in-depth study of the SAT problem itself, but also provided strong support for the development of computer science, artificial intelligence and other related fields. Currently, the research of SAT problem involves several aspects, this paper mainly focuses on the three aspects of the improvement of SAT solving algorithm, the deepening of the theoretical foundation of SAT and the expansion of the application area to sort out the related research results, summarize the limitations of the existing methods, and propose possible future work.

Downloads

Download data is not yet available.

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.

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.

Ruiz R, Pranzo M. Stochastic Local Search: Foundations and Applications,Holger H. Hoos, Thomas Stützle, Morgan Kaufmann Publishers[J]. European Journal of Operational Research, 2006,172(2):716-718.

Yung W H, Seung Y W, Lee K H, et al. A Runtime Reconfigurable Implementation of the GSAT Algorithm[J]. Springer-Verlag, 1999.

Selman B, Kautz H A, Cohen B. Local Search Strategies for Satisfiability Testing[J]. cliques coloring & satisfiability second dimacs implementation challenge, 1996.

Balint A, Fröhlich A. Improving Stochastic Local Search for SAT with a New Probability Distribution: Theory and Applications of Satisfiability Testing – SAT 2010[C], 2010.

S. C, K. S. Local Search with Configuration Checking for SAT: IEEE 23rd International Conference on Tools with Artificial Intelligence[C], 2011.

A B, U S. Choosing probability distributions for stochastic local search and the role of make versus break: Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing[C], 2012.

Liu S, Papakonstantinou P. Local Search for Hard SAT Formulas: The Strength of the Polynomial Law: Proceedings of the AAAI Conference on Artificial Intelligence[C], 2016.

Hossen M S, Polash M M A. Implementing an Efficient SAT Solver for Structured Instances: 2019 Joint 8th International Conference on Informatics, Electronics & Vision (ICIEV) and 2019 3rd International Conference on Imaging, Vision & Pattern Recognition (icIVPR)[C], Spokane, WA, USA, 2019.

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.

Devlin D, O Sullivan B. Satisfiability as a Classification Problem.: In Proc. of the 19th Irish Conf. on Artificial Intelligence andCognitive Science[C], 2008.

Danisovszky M Z G Y. Classification of SAT Problem Instances by Machine Learning Methods: International Conference on Applied Informatics[C], 2020.

Liang J H, Oh C, Mathew M, et al. Machine Learning-Based Restart Policy for CDCL SAT Solvers: Theory and Applications of Satisfiability Testing – SAT 2018[C], 2018.

Wang Y, Cn Y S N E, Fengjuan G A A L. CNNSAT: Fast, Accurate Boolean Satisfiability using Convolutional Neural Networks: ICLR[C], 2019.

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.

Mazyavkina N, Sviridov S, Ivanov S, et al. Reinforcement learning for combinatorial optimization: A survey[J]. Computers & Operations Research, 2021,134:105400.

Wang F, Rompf T. From Gameplay to Symbolic Reasoning: Learning SAT Solver Heuristics in the Style of Alpha(Go) Zero[J]. ArXiv, 2018.

Selsam D, Lamm M, Bünz B, et al. Learning a SAT Solver from Single-Bit Supervision: International Conference on Learning Representations[C], 2018.

Selsam D, Bjørner N. Guiding High-Performance SAT Solvers with Unsat-Core Predictions: Theory and Applications of Satisfiability Testing – SAT 2019[C], 2019.

Zhang W, Sun Z, Zhu Q, et al. NLocalSAT: Boosting Local Search with Solution Prediction: Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence[C], 2020.

Chang W, Zhang H, Luo J. Predicting Propositional Satisfiability Based on Graph Attention Networks[J]. International Journal of Computational Intelligence Systems, 2022,15(1):84.

Shi Z, Li M, Khan S, et al. SATformer: Transformers for SAT Solving[J]. arXiv preprint, 2022.

Shi F, LI C, Bian S, et al. Transformers satisfy: ICLR[C], 2021.

Arora, Sanjeev, Barak B. Computational Complexity: A Modern Approach[M]. Cambridge University Press40 W. 20 St. New York, NYUnited States, 2009.

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.

Downey R, Flum J, Grohe M, et al. Bounded fixed-parameter tractability and reducibility[J]. Annals of Pure and Applied Logic, 2007,148(1):1-19.

Biere A, Cimatti A, Clarke E M, et al. Symbolic model checking using SAT procedures instead of BDDs: Proceedings 1999 Design Automation Conference[C], New Orleans, LA, USA, 1999.

Biere A, Cimatti A, Clarke E, et al. Symbolic Model Checking without BDDs: Tools and Algorithms for the Construction and Analysis of Systems[C], 1999.

Larrabee T. Test pattern generation using Boolean satisfiability[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992,11(1):4-15.

Chen P, Keutzer K. Towards true crosstalk noise analysis: 1999 IEEE/ACM International Conference on Computer-Aided Design. Digest of Technical Papers [C], San Jose, CA, USA, 1999.

Jackson D, Schechter I, Shlyakhter I. Alcoa: the Alloy constraint analyzer: Proceedings of the 2000 International Conference on Software Engineering[C], Limerick, Ireland, 2000.

Muise C, McIlraith S A, Beck J C, et al. Dsharp: Fast d-DNNF Compilation with sharpSAT: Advances in Artificial Intelligence[C], 2012.

Rintanen J. Planning as satisfiability: Heuristics[J]. Artificial Intelligence, 2012,193:45-86.

Rintanen J, Heljanko K, Niemelä I. Planning as satisfiability: parallel plans and algorithms for plan search[J]. Artificial Intelligence, 2006,170(12):1031-1080.

Appel K, Haken W. The solution of the four-color-map problem[J]. Scientific African, 2010,4(237):108-121.