严格随机正则(3,s)-SAT模型及其相变现象

研究变元和文字出现次数受限制的规则3-SAT问题，提出了一种严格随机正则（3，s）-SAT问题，并给出了该问题的实例产生模型--SRR模型。结合一阶矩方法和生成函数展开项系数的渐近近似技术，证明了严格随机正则（3，s）-SAT问题相变点的上界，即当变元规模N较大且变元出现次数s>11时，严格随机正则（3，s）-SAT实例是高概率不可满足的。实验结果表明：由SRR模型所生成的随机实例中，当N>60且s>11时，所有的（3，s）-SAT实例均是不可满足的，而当N>150且s<11时，所有的（3，s）-SAT实例均是可满足的，即严格随机正则（3，s）-SAT实例的相变点位于s=11处，且在s=11处（子句变元比为11/3）的严格随机正则（3，s）-SAT实例，比在相变点（子句变元比）4.267处同规模的均匀随机3-SAT实例更难求解，因此，SRR模型可以很方便地在s=11处构造难解的随机3-SAT实例。

Strictly regular random (3, s)-SAT model and its phase transition phenomenon

We study the restricted occurrence times for variables and literatures in 3-SAT problem. In particular, we propose a strictly regular random (3,s)-SAT problem and its instances generating model-SRR model. Using the first moment method and the asymptotic approximation technique to the expansion coefficient in generating function, we derive an upper bound of the phase transformation point for the strictly regular random (3,s)-SAT problem, i.e., when the variable size N is large enough and the variable occurrence times s is greater than 11, the strictly regular random (3,s)-SAT instances are unsatisfied with high probability. Furthermore, for the random instances generated by model SRR with different variable size, our experimental results show that when N is greater than 60 and s is greater than 11, all the (3,s)-SAT instances are unsatisfied, and when N is greater than 150 and s is less than 11, all the (3,s)-SAT instances are satisfied. Thus, the phase transition point of the strictly regular random (3,s)-SAT instances is located at s=11(i.e., the ratio of clauses to variables is 11/3). We also observe that the strictly regular random (3,s)-SAT instances at the location s=11 are much more difficult to solve than the uniform random 3-SAT instances around its phase transition point, which is about 4.267 (the ratio of clauses to variables). Therefore, it is quite easy to generate hard random 3-SAT instances by our SRR model at the location where s is 11.