CNF公式赋值空间的结构信息与聚类性质

论文摘要

可满足性问题备受计算机科学众多领域的关注,不同形式的组合约束问题都可以在多项式时间内转化为可满足性问题。一种广泛用于研究可满足性问题的方法是将其转换成因子图的形式表示,因子图作为一种推理变元边缘概率的工具,用于各种信息传播算法中,有效的提高了求解可满足性问题的效率。通过关注因子图上变元、子句本身的结构信息来探究CNF公式的可满足性,或者通过数据挖掘技术分析子句、变元之间潜在的结构信息。因此,CNF公式所隐含的结构信息为探究可满足性问题提供了新的方法。本文以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一类有向图--BF图,期望通过BF图上的结构信息来探究可满足解之间的关系,从而研究合取范式公式赋值空间在可满足的情况下的结构性质和聚类现象,为求解SAT问题提供新的思路。本文的主要研究结果有:（1）给出了在BF图上进行随机游走获得可满足解的概率性质。对于含有n个变元m个子句的CNF公式,随着翻转控制参数k的增大,在其BF图上取得可满足解的概率也相应增大,当k靠近n时,概率稳定。对于可满足的CNF公式,在其任意k值下的BF图上进行t次随机游走,当t足够大时,取得可满足解的概率最终会收敛于1。最后,通过实验仿真支持性质的正确性。（2）通过对CNF公式赋值空间中可满足解进行分析探究聚类现象。CNF公式赋值空间中存在可满足解聚集成簇的现象,且解聚类的个数随着约束密度的变化而发生改变,符合统计物理学中复本对称破缺平均场理论的对解空间的物理图景描述。本文通过引入有效部分指派,约束变元等相关知识发现:每一个可满足解中有唯一的核,且属于同一个聚类中的可满足解有相同的核。

论文目录

• 摘要
• Abstract
• 第一章 绪论
•   1.1 研究背景和意义
•   1.2 国内外研究现状
•   1.3 论文研究内容
•   1.4 论文结构
• 第二章 基础知识
•   2.1 可满足性问题
•   2.2 命题公式的因子图
•   2.3 相变现象
•   2.4 马尔可夫链
•   2.5 本章小结
• 第三章 带变量控制参数的BF图的构造与示例
•   3.1 带变量翻转控制参数的BF图
•   3.2 BF图实例构造
•   3.3 本章小结
• 第四章 带变量控制参数的BF图的结构性质
•   4.1 BF图上的基本结构性质
•   4.2 带变量控制参数的BF图的性质研究
•   4.3 图上性质研究的实验仿真与分析
•   4.4 控制参数k的合适取值
•   4.5 本章小结
• 第五章 CNF公式赋值空间的聚类现象
•   5.1 赋值空间中的聚类现象
•   5.2 解空间的聚类性质
•   5.3 本章小结
• 第六章 总结与展望
•   6.1 论文总结
•   6.2 展望
• 致谢
• 参考文献
• 附录
• 图版

文章来源

类型: 硕士论文

作者: 莫孝玲

导师: 许道云

关键词: 公式,赋值空间,翻转控制参数,可满足解,聚类

来源: 贵州大学

年度: 2019

分类: 基础科学

专业: 数学

单位: 贵州大学

分类号: O157.5

总页数: 57

文件大小: 1417K

下载量: 16