On the upper bounds of (1,0)-super solutions for the regular balanced random (k,2s)-SAT problem

Abstract

This paper explores the conditions which make a regular balanced random (k,2s)-CNF formula (1,0)-unsatisfiable with high probability. The conditions also make a random instance of the regular balanced (k-1,2(k-1)s)-SAT problem unsatisfiable with high probability, where the instance obeys a distribution which differs from the distribution obeyed by a regular balanced random (k-1,2(k-1)s)-CNF formula. Let \mathbf{F} be a regular balanced random (k,2s)-CNF formula where k\ge 3, then there exists a number s_0 such that \mathbf{F} is (1,0)-unsatisfiable with high probability if s>s_0. A numerical solution of the number s_0 when k\in \{5,6,\dots ,14\} is given to conduct simulated experiments. The simulated experiments verify the theoretical result. Besides, the experiments also suggest that \mathbf{F} is (1,0)-satisfiable with high probability if s is less than a certain value.

Graphical abstract

Keywords

regular balanced random (k,2s)-SAT problem / (1,0)-super solution / upper bound

Yongping Wang received the PhD degree from Guizhou University, China in 2020. He is an associate professor at School of Information, Guizhou University of Finance and Economics, China. His research interests include computability and computational complexity, and algorithm design and analysis

Daoyun Xu received the PhD degree from Nanjing University, China in 2002. He is a professor and PhD supervisor at College of Computer Science and Technology, Guizhou University, China, and the senior member of CCF. His research interests include computability and computational complexity, and algorithm design and analysis

Jincheng Zhou received the PhD degree from Guizhou University, China in 2016. He is a professor and master supervisor at School of Computer and Information, Qiannan Normal University for Nationalities, China, and the senior member of CCF. His research interests include computational complexity, and algorithm design and analysis

References

[1] Ginsberg M L, Parkes A J, Roy A. Supermodels and robustness. In: Proceedings of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference. 1998, 334−339

[2] Hebrard E, Hnich B, Walsh T. Super solutions in constraint programming. In: Proceedings of the 1st International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. 2004, 157−172

[3] Zhang P, Gao Y . A probabilistic study of generalized solution concepts in satisfiability testing and constraint programming. Theoretical Computer Science, 2017, 657: 98–110

[4] Cook S A. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. 1971, 151−158

[5] Mitchell D, Selman B, Levesque H. Hard and easy distributions of SAT problems. In: Proceedings of the 10th National Conference on Artificial Intelligence. 1992, 459−465

[6] Friedgut E, Bourgain J . Sharp thresholds of graph properties, and the k-SAT problem. Journal of the American Mathematical Society, 1999, 12( 4): 1017–1054

[7] Chvátal V, Reed B. Mick gets some (the odds are on his side) . In: Proceedings of the 33rd Annual Symposium on Foundations of Computer Science. 1992, 620−627

[8] Kaporis A C, Kirousis L M, Lalas E G . The probabilistic analysis of a greedy satisfiability algorithm. Random Structures & Algorithms, 2006, 28( 4): 444–480

[9] Díaz J, Kirousis L, Mitsche D, Pérez-Giménez X . On the satisfiability threshold of formulas with three literals per clause. Theoretical Computer Science, 2009, 410( 30−32): 2920–2934

[10] Chao M T, Franco J . Probabilistic analysis of two heuristics for the 3-satisfiability problem. SIAM Journal on Computing, 1986, 15( 4): 1106–1118

[11] Achioptas D, Sorkin G B. Optimal myopic algorithms for random 3-SAT. In: Proceedings of the 41st Annual Symposium on Foundations of Computer Science. 2000, 590−600

[12] Braunstein A, Mézard M, Zecchina R . Survey propagation: an algorithm for satisfiability. Random Structures & Algorithms, 2005, 27( 2): 201–226

[13] Zhou G, Kang R . On the lower bounds of (1,0)-super solutions for random k-SAT. International Journal of Foundations of Computer Science, 2019, 30( 2): 247–254

[14] Wang B, Zhou G . Super solutions of random (3+p)-SAT. Theoretical Computer Science, 2019, 793: 14–27

[15] Zhou J C, Xu D Y, Lu Y J . Satisfiability threshold of the regular random (k,r)-SAT problem. Journal of Software, 2016, 27( 12): 2985–2993

[16] Boufkhad Y, Dubois O, Interian Y, Selman B . Regular random k-SAT: properties of balanced formulas. Journal of Automated Reasoning, 2005, 35( 1−3): 181–200

[17] Rathi V, Aurell E, Rasmussen L, Skoglund M. Bounds on threshold of regular random k-SAT. In: Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing. 2010, 264−277

[18] Sumedha , Krishnamurthy S, Sahoo S . Balanced K-satisfiability and biased random K-satisfiability on trees. Physical Review E, 2013, 87( 4): 042130

[19] Zhou J, Xu D, Lu Y, Dai C . Strictly regular random (3,s)-SAT model and its phase transition phenomenon. Journal of Beijing University of Aeronautics and Astronautics, 2016, 42( 12): 2563–2571

[20] Zhou J, Xu D, Lu Y . Satisfiability threshold of regular (k,r)-SAT problem via 1RSB theory. Journal of Huazhong University of Science and Technology: Natural Science Edition, 2017, 45( 12): 7–13

[21] Coja-Oghlan A, Wormald N . The number of satisfying assignments of random regular k-SAT formulas. Combinatorics, Probability and Computing, 2018, 27( 4): 496–530

[22] Achlioptas D, Peres Y . The threshold for random k-SAT is 2^klog2-O(k). Journal of the American Mathematical Society, 2004, 17( 4): 947–973

[23] Mahajan Y S, Fu Z, Malik S. Zchaff2004: an efficient SAT solver. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing. 2005, 360−375

[24] Wang Y, Xu D . Properties of the satisfiability threshold of the strictly d-regular random (3,2s)-SAT problem. Frontiers of Computer Science, 2020, 14( 6): 146404

[25] Gardy D . Some results on the asymptotic behaviour of coefficients of large powers of functions. Discrete Mathematics, 1995, 139( 1−3): 189–217

[26] Richardson T, Urbanke R. Modern Coding Theory. London: Cambridge University Press, 2008

Acknowledgements

The authors would like to thank the Scientific Research Project for Introduced Talents of Guizhou University of Finance and Economics (No. 2021YJ007), the National Natural Science Foundation of China (Grant Nos. 61862051, 61762019, 62241206), the Top-notch Talent Program of Guizhou Province (No. KY[2018]080), the Science and Technology Foundation of Guizhou Province (No. 20191299), and the foundation of Qiannan Normal University for Nationalities (Nos. QNSYRC201715, QNSY2018JS013).

RIGHTS & PERMISSIONS

2024 Higher Education Press