北京航空航天大学学报 ›› 2016, Vol. 42 ›› Issue (12): 2563-2571.doi: 10.13700/j.bh.1001-5965.2015.0845

• 论文 • 上一篇    下一篇

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

周锦程1,2, 许道云1, 卢友军1, 代寸宽1   

  1. 1. 贵州大学 计算机科学与技术学院, 贵阳 550025;
    2. 黔南民族师范学院 数学与统计学院, 都匀 558000
  • 收稿日期:2015-12-24 出版日期:2016-12-20 发布日期:2016-04-13
  • 通讯作者: 许道云,Tel.:0851-83627649,E-mail:dyxu@gzu.edu.cn E-mail:dyxu@gzu.edu.cn
  • 作者简介:周锦程,男,博士研究生,副教授。主要研究方向:计算复杂性、算法设计与分析、SAT问题等。Tel.:13809490127,E-mail:guideaaa@126.com;许道云,男,博士,教授,博士生导师。主要研究方向:可计算性与计算复杂性、算法设计与分析、SAT问题等。Tel.:0851-83627649,E-mail:dyxu@gzu.edu.cn
  • 基金资助:
    国家自然科学基金(61262006,61463044,61462001);贵州省重大应用基础研究项目(JZ20142001);贵州省科技厅联合基金(LH20147636,LKQS201313);黔南民族师范学院校级科研项目(QNSY2011QN10,2014ZCSX13)

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

ZHOU Jincheng1,2, XU Daoyun1, LU Youjun1, DAI Cunkuan1   

  1. 1. College of Computer Science and Technology, Guizhou University, Guiyang 550025, China;
    2. School of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, China
  • Received:2015-12-24 Online:2016-12-20 Published:2016-04-13
  • Supported by:
    National Natural Science Foundation of China (61262006, 61463044, 61462001); Major Applied Basic Research Program of Guizhou Province (JZ20142001); Science and Technology Foundation of Guizhou Province (LH20147636, LKQS201313); the Foundation of Qiannan Normal University for Nationalities (QNSY2011QN10, 2014ZCSX13)

摘要: 研究变元和文字出现次数受限制的规则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实例。

关键词: 严格正则(3,s)-SAT问题, 相变性质, 计算复杂性, 难解实例产生模型, 生成函数

Abstract: 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.

Key words: strictly regular (3,s)-SAT problem, phase transition properties, computational complexity, hard instances generation model, generating function

中图分类号: 


版权所有 © 《北京航空航天大学学报》编辑部
通讯地址:北京市海淀区学院路37号 北京航空航天大学学报编辑部 邮编:100191 E-mail:jbuaa@buaa.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发