Properties of the satisfiability threshold of the strictly d-regular random (3, 2s)-SAT problem
Yongping WANG1,2, Daoyun XU1()
1. College of Computer Science and Technology, Guizhou University, Guiyang 550025, China 2. College of Mathematics and Statistics, Guizhou University of Finance and Economics, Guiyang 550025, China
A k-CNF (conjunctive normal form) formula is a regular (k, s)-CNF one if every variable occurs s times in the formula, where k≥2 and s>0 are integers. Regular (3, s)- CNF formulas have some good structural properties, so carrying out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysis for random 3-CNF formulas. Some subclasses of the regular (3, s)-CNF formula have also characteristics of intractability that differ from random 3-CNF formulas. For this purpose, we propose strictly d-regular (k, 2s)-CNF formula, which is a regular (k, 2s)-CNF formula for which d≥0 is an even number and each literal occurs or times (the literals from a variable x are x and , where x is positive and is negative). In this paper, we present a new model to generate strictly d-regular random (k, 2s)-CNF formulas, and focus on the strictly d-regular random (3, 2s)-CNF formulas. Let F be a strictly d-regular random (3, 2s)-CNF formula such that 2s>d. We show that there exists a real number s0 such that the formula F is unsatisfiable with high probability when s>s0, and present a numerical solution for the real number s0. The result is supported by simulated experiments, and is consistent with the existing conclusion for the case of d= 0. Furthermore, we have a conjecture: for a given d, the strictly d-regular random (3, 2s)-SAT problem has an SAT-UNSAT (satisfiable-unsatisfiable) phase transition. Our experiments support this conjecture. Finally, our experiments also show that the parameter d is correlated with the intractability of the 3-SAT problem. Therefore, our research maybe helpful for generating random hard instances of the 3-CNF formula.
S A Cook. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. 1971, 151–158 https://doi.org/10.1145/800157.805047
2
E Friedgut, J Bourgain. Sharp thresholds of graph properties, and the k-SAT problem. Journal of the American Mathematical Society, 1999, 12(4): 1017–1054 https://doi.org/10.1090/S0894-0347-99-00305-7
3
A C Kaporis, L M Kirousis, E G Lalas. The probabilistic analysis of a greedy satisfiability algorithm. Random Structures & Algorithms, 2006, 28(4): 444–480 https://doi.org/10.1002/rsa.20104
4
J Díaz, L Kirousis, D Mitsche, X Pérez-Giménez. On the satisfiability threshold of formulas with three literals per clause. Theoretical Computer Science, 2009, 410(30–32): 2920–2934 https://doi.org/10.1016/j.tcs.2009.02.020
5
D Mitchell, B Selman, H Levesque. Hard and easy distributions of SAT problems. In: Proceedings of the 10th National Conference on Artificial Intelligence. 1992, 459–465
6
J M Crawford, L D Auton. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, 1996, 81(1–2): 31–57 https://doi.org/10.1016/0004-3702(95)00046-1
7
R Monasson, R Zecchina, S Kirkpatrick, B Selman, L Troyansky. Determining computational complexity from characteristic ‘phase transitions’. Nature, 1999, 400(6740): 133–137 https://doi.org/10.1038/22055
8
A Braunstein, M Mézard, R Zecchina. Survey propagation: an algorithm for satisfiability. Random Structures & Algorithms, 2002, 27(2): 201–226 https://doi.org/10.1002/rsa.20057
9
D Xu, X Wang. A regular NP-complete problem and its inapproximability. Journal of Frontiers of Computer Science and Technology, 2013, 7(8): 691–697 (In Chinese)
10
Y Boufkhad, O Dubois, Y Interian, B Selman. Regular random k-SAT: properties of balanced formulas. Journal of Automated Reasoning, 2005, 35(1–3): 181–200 https://doi.org/10.1007/s10817-005-9012-z
11
V Rathi, E Aurell, L Rasmussen, M Skoglund. Bounds on threshold of regular random k-SAT. In: Proceedings of the 13th International Conference on Theory & Applications of Satisfiability Testing. 2010, 264–277 https://doi.org/10.1007/978-3-642-14186-7_22
12
J Zhou, D Xu, Y Lu, C Dai. 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 (In Chinese)
13
D Gardy. Some results on the asymptotic behaviour of coefficients of large powers of functions. Discrete Mathematics, 1995, 139(1–3): 189–217 https://doi.org/10.1016/0012-365X(94)00133-4
14
Y S Mahajan, Z Fu, S Malik. Zchaff2004: an efficient SAT solver. In: Proceedings of the 7th International Conference on Theory & Applications of Satisfiability Testing. 2004, 360–375 https://doi.org/10.1007/11527695_27
15
J C Zhou, D Y Xu, Y J Lu. Satisfiability threshold of the regular random (k, r)-SAT problem. Ruan Jian Xue Bao/Journal of Software, 2016, 27(12): 2985–2993 (In Chinese)
16
S Sumedha, Krishnamurthy, S Sahoo. Balanced k-satisfiability and biased random k-satisfiability on trees. Physical Review E, 2013, 87(4): 042130 https://doi.org/10.1103/PhysRevE.87.042130