Abstract:Generating random hard instances of the 3-CNF formula is an important factor in revealing the intractability of the 3-SAT problem and designing effective algorithms for satisfiability testing. Let k>2 and s>0 be integers, a k-CNF formula is a strictly regular (k,2s)-CNF one if the positive and negative occurrence number of every variable in the formula are s. On the basis of the strictly regular (k,2s)-CNF formula, the strictly d-regular (k,2s)-CNF formula is proposed in which the absolute value of the difference between positive and negative occurrence number of every variable is d. A novel model is constructed to generate the strictly d-regular random (k,2s)-CNF formula. The simulated experiments show that the strictly d-regular random (3,2s)-SAT problem has an SAT-UNSAT phase transition and a HARD-EASY phase transition when the parameter 5<s<11 is fixed, and that the latter is related to the former. Hence, the satisfiability threshold of the strictly d-regular random (3,2s)-SAT problem is studied when the parameter s is fixed. A lower bound of the satisfiability threshold is obtained by constructing a random experiment and using the first moment method. The subsequent simulated experiments verify well the lower bound proved.