平衡正则(k,2r)-CNF公式结构信息及相变性质

摘要

布尔可满足性问题是理论计算机科学中的核心问题，人们一直致力于寻找CNF公式实例难解的本质，通过限定CNF公式的结构，如子句长度、布尔变元出现次数等，并以此为基础，分析CNF公式的结构信息，设计高效的求解算法。本文研究的平衡正则(k,2r)-CNF公式是一类具有规则结构的CNF公式，通过限定每个子句的长度为k，每个布尔变元的正出现次数和负出现次数都为r，其实例求解难度比一般的k-CNF公式实例求解难度大。本文从实例生成模型、结构信息、求解算法、相变性质等方面对平衡正则(k,2r)-CNF公式进行研究，主要研究成果如下： （1）为了便于分析平衡正则(k,2r)-CNF公式的结构信息及相变性质，构建了一个生成平衡正则(k,2r)-CNF公式实例的随机模型—BR(n,k,2r)模型。该模型可以有效地生成不重复的平衡正则(k,2r)-CNF公式子句。 （2）通过将平衡正则(k,2r)-CNF公式分别表示为变元交互图和因子图，研究了平衡正则(k,2r)-CNF公式的结构信息。实验发现：在变元交互图中，顶点的度与公式的子句变元比正相关；在因子图中，子句与变元呈现交错分布。 （3）基于平衡正则(k,2r)-CNF公式特殊的结构信息，改进了随机局部搜索（Stochastic Local Search，SLS）算法的初始赋值方式来求解该类正则公式。实验结果表明：改进后的SLS算法比原算法能更有效地求解平衡正则(k,2r)-CNF公式。 （4）平衡正则(k,2r)-CNF公式实例随着子句变元比的增大，会出现可满足性相变现象。通过理论分析，给出了平衡正则(k,2r)-CNF公式可满足性相变阈值点的一个上界为2k ln2?kln2/2，一个下界为2k ln2?kln2/2?2ln2.

目录

第一章 绪论

1.1研究背景和意义

1.2国内外研究现状

1.3论文研究内容

1.4论文结构

第二章 基础知识

2.1平衡正则(k,2r)-CNF公式

2.2布尔可满足性问题

2.3 因子图

2.4 矩方法

第三章平衡正则(k, 2r)-CNF公式的结构信息分析

3.1BR(n,k, 2r)模型

3.2 变元交互图分析

3.3 因子图分析

第四章平衡正则(k, 2r)-CNF公式的求解算法

4.1 完备性算法

4.2 非完备性算法

4.3 SLS算法改进

4.4 实验设计与分析

第五章平衡正则(k, 2r)-CNF公式的相变性质

5.1相变现象

5.2 理论分析

第六章 总结与展望

致谢

参考文献

附录

图版

表版

声明