为分析合取范式(conjunctive normal form,CNF)公式的赋值空间在可满足性情况下的结构性质,引入一个变元翻转次数控制的参数k,k不小于1且不大于n,n为公式中出现的变元个数,以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一...为分析合取范式(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。最后,实验仿真支持性质的正确性。展开更多
基金Supported by the National Natural Science Foundation of China(62173308,61973078)the Natural Science Foundation of Zhejiang Province of China(LR20F030001,LD19A010001)。
文摘为分析合取范式(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。最后,实验仿真支持性质的正确性。
