Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2020, Vol. 14 Issue (6) : 146404    https://doi.org/10.1007/s11704-020-9248-0
RESEARCH ARTICLE
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
 Download: PDF(320 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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 sd2 or s+d2 times (the literals from a variable x are x and ¬x, where x is positive and ¬x 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
 Cite this article:   
Yongping WANG,Daoyun XU. Properties of the satisfiability threshold of the strictly d-regular random (3, 2s)-SAT problem[J]. Front. Comput. Sci., 2020, 14(6): 146404.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-020-9248-0
https://academic.hep.com.cn/fcs/EN/Y2020/V14/I6/146404
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