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

摘要

为分析合取范式(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.最后,实验仿真支持性质的正确性.