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

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-<mml:mfrac>d2</mml:mfrac> or s+<mml:mfrac>d2</mml:mfrac> times (the literals from a variable x are x and not signx, where x is positive and not signx 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(0) such that the formula F is unsatisfiable with high probability when s > s(0), and present a numerical solution for the real number s(0). 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.