|
|
|
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 |
|
|
|
|
Abstract 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.
|
| Keywords
satisfiability problem
SAT-UNSAT phase transition
generating random hard instances
|
|
Corresponding Author(s):
Daoyun XU
|
|
Just Accepted Date: 04 March 2020
Issue Date: 20 July 2020
|
|
| 1 |
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|