摘要
为分析合取范式(conjunctive normal form,CNF)公式的赋值空间在可满足性情况下的结构性质,引入一个变元翻转次数控制的参数k,k不小于1且不大于n,n为公式中出现的变元个数,以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一类有向图——BF(bounded flips)图。研究带翻转控制参数的BF图的若干基础性质,根据BF图的性质研究CNF公式可满足解的概率性质。对于含有n个变元m个子句CNF公式,随着翻转控制参数k的增大,在其BF图上取得可满足解的概率也相应增大。当k靠近n时,概率稳定。对于可满足的CNF公式,在其任意k值下的BF图上进行t次随机游走。当t足够大时,取得可满足解的概率最终会收敛于1。最后,实验仿真支持性质的正确性。
To analyze the structural properties of the CNF(conjunctive normal form)formula's assignment space under the condition of satisfiability,a parameter k is introduced to control the number of times of variable flipping.k is not less than 1 and it's not greater than n,where n is the number of variable appearing in the formula.Assignment is taken as the node and based on the size of the number of clauses satisfied under the control of the flip boundary,a type of directed graph--BF(bounded flips)graph is introduced.In this paper,some basic properties of BF graphs with flipping control parameters are investigated,and based on this to study the probabilistic properties of satisfiable solutions of CNF formula.It is found that for a CNF formula with n variables and m clauses,the probability of obtaining a satisfiable solution on the BF graph increases with the increase of flip control parameter k.What's more,when the parameter k approaches n,the probability is stable.It proves that for a satisfiable CNF formula,t steps random walks are performed on BF graphs with arbitrary k-values.When t is large enough,the probability of obtaining a satisfiable solution will eventually converge to 1.Finally,experimental simulation supports the correctness of the property.
作者
莫孝玲
许道云
MO Xiaoling;XU Daoyun(College of Computer Science and Technology,Guizhou University,Guiyang 550025,China)
出处
《计算机科学与探索》
CSCD
北大核心
2018年第11期1852-1861,共10页
Journal of Frontiers of Computer Science and Technology
基金
国家自然科学基金Nos.61762019
61462001~~
关键词
合取范式(CNF)公式
赋值空间
翻转控制参数
可满足解
conjunctive normal form(CNF)formula
assignment space
flip control parameter
satisfiable solution
