Properties of the satisfiability threshold of the strictly d-regular random (3, 2s)-SAT problem

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 s-\frac{d}{2} or s+\frac{d}{2} times (the literals from a variable x are x and \neg x, where x is positive and \neg 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 s₀ such that the formula F is unsatisfiable with high probability when s>s₀, and present a numerical solution for the real number s₀. 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

References

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

[2] 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

[3] 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

[4] 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

[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] Crawford J M, Auton L D. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, 1996, 81(1–2): 31–57

[7] Monasson R, Zecchina R, Kirkpatrick S, Selman B, Troyansky L. Determining computational complexity from characteristic ‘phase transitions’. Nature, 1999, 400(6740): 133–137

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

[9] Xu D, Wang X. A regular NP-complete problem and its inapproximability. Journal of Frontiers of Computer Science and Technology, 2013, 7(8): 691–697 (In Chinese)

[10] 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

[11] 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 & Applications of Satisfiability Testing. 2010, 264–277

[12] 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 (In Chinese)

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

[14] Mahajan Y S, Fu Z, Malik S. Zchaff2004: an efficient SAT solver. In: Proceedings of the 7th International Conference on Theory & Applications of Satisfiability Testing. 2004, 360–375

[15] Zhou J C, Xu D Y, Lu Y J. 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] Sumedha, Krishnamurthy S, Sahoo S. Balanced k-satisfiability and biased random k-satisfiability on trees. Physical Review E, 2013, 87(4): 042130

RIGHTS & PERMISSIONS

2020 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature