CNF公式赋值空间上可满足解的概率性质

Probabilistic Properties of Satisfiable Solutions on Space of Assignments for CNF Formula

为分析合取范式(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.