布尔满足性判定算法研究

摘要

布尔满足性判定问题是多个不同学科的交叉问题，它是一类著名的NP-完全问题。但是，随着布尔满足性判定算法性能的不断提升，它已经被大量的应用于实际问题的求解，如组合电路等价性检测、自动测试模板生成、软件模式检测、满足模块定理证明、计算生物学和自动规划等。大量具有不同特性的布尔满足性判定算法被设计和优化，以实现对实际问题的快速求解。但是，部分问题求解的时间复杂度和空间复杂度还有待进一步降低，很多难实例问题仍然在有限的时间内无法求解。针对特定问题类的高效布尔满足性判定算法一直是计算机及人工智能领域的热点研究问题之一。
　　本文在深入研究布尔满足性判定算法的基础上，针对不同的问题进行了建模和算法设计，其主要研究内容分为四部分。
　　1、针对Model RB模型的特性，通过集合和图的方式对问题进行了形式化建模和描述，融合完全布尔满足性判定算法和随机布尔满足性判定算法的不同优势，实现了高效的完全布尔满足性判定算法。基于完全布尔满足性判定算法的基本搜索流程，提出了基于互斥集和关联集的搜索判定算法。在搜索过程中，根据动态生成的子句集构造搜索树、选择决策变量并确定回退机制。为实现搜索过程中的快速冲突回退，使用随机算法获得图中的最大团，并利用最大团中的节点构造初始搜索树。实验结果显示，算法在Model RB模型和图着色问题实例中具有较好的性能。
　　2、随着人们对基因认识的不断深入和基因序列提取能力的不断增强，计算生物学对基因的研究已经从单基因的性质研究逐渐转向对基因调控网络的动态特性研究。在基因调控网络研究中的一个重要问题是吸引子的求解问题，吸引子代表基因网络的稳定状态，一个吸引子表示一种细胞类型。基于同步布尔网络建模的方式，将基因调控网络的动态调控过程转化成了同步布尔网络的状态转换图。为降低状态转换图中吸引子的求解复杂度，以布尔网络中的强连通分支为单位将布尔网络划分成了多个块，各个块之间形成有向无环的依赖关系。算法通过计算每一个块的局部吸引子来获得整个网络的吸引子。在计算局部吸引子时，算法通过展开布尔网络转换函数的方式将吸引子求解问题转换成布尔满足性判定问题进行求解。实验结果表明，基于分块的吸引子求解算法针对复杂的基因调控网络具有显著的优势。
　　3、为充分利用计算机多核的处理能力，实现高效的问题求解，并行计算已经成为一种必然的软件设计趋势。在深入研究并行布尔满足性判定算法的基础上，结合基于分块的算法特性，设计并实现了两种并行的吸引子求解算法：基于块的并行算法和基于局部吸引子的并行算法。基于块的并行算法使用空间划分的方式实现并行布尔满足性判定求解，而基于局部吸引子的并行算法在空间划分的基础上实现了负载均衡。基于块的并行算法在计算完第一个节点块的所有局部吸引子后，将局部吸引子平均分配给所有CPU的核进行后续的节点块计算。基于局部吸引子的并行算法计算完一个局部吸引子就会产生一个消息，通知空闲CPU核进行后续的计算。实验结果表明，并行吸引子求解的性能优于串行求解的性能，基于局部吸引子的并行算法优于基于块的并行算法。特别是当CPU的核数较多时，基于局部吸引子的并行算法优势更加突出。
　　4、布尔网络稳定态的计算是一个NP完全问题，大量的实例无法在有限的时间内获得所有的稳定状态。为能够对问题进行初步的分析，提出了一种计算小于等于给定环长的所有稳定态的算法。算法基于边界模式检测技术对问题进行建模，基于变量分类、蕴含图的决策变量生成阻塞子句等技术对布尔满足性判定全解算法进行了优化。实现结果表明，算法对于环长分布比较均匀的布尔网络具有较低的计算复杂度，特别是对于无法计算所有环的复杂网络，算法更具有应用价值。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪 论

1.1 研究工作的背景与意义

1.2 布尔满足性判定算法的国内外研究历史与现状

1.3 布尔满足性判定算法的应用

1.4 本文的主要贡献与创新

1.5 本论文的结构安排

第二章 完全布尔满足判定算法相关技术

2.1 基本概念

2.2 问题转换成CNF范式

2.3 完全SAT算法基本流程

2.4 完全SAT算法优化技术

2.5 本章小结

第三章 基于集合和图的完全布尔满足性判定算法

3.1 问题描述

3.2 形式化建模

3.3 R-SAT算法

3.4 RC-SAT和RIC-SAT算法

3.5算法的图着色应用

3.6实验结果分析

3.7 本章小结

第四章 基于分块的布尔网络吸引子求解算法

4.1 问题描述

4.2 布尔网络建模

4.3 布尔网络模型的吸引子求解相关算法

4.4 基于SAT的布尔网络吸引子求解算法

4.5 基于分块的吸引子求解算法

4.6 实验结果分析

4.7 本章小结

第五章 布尔网络吸引子并行求解算法

5.1 问题描述

5.2 基于空间划分的并行SAT算法

5.3 基于分块的并行算法

5.4 实验结果分析

5.5 本章小结

第六章 布尔网络稳定态求解算法

6.1 问题描述

6.2 边界模式检测的问题描述方式

6.3 全解SAT求解算法

6.4 指定步长的环求解算法

6.5 实验结果分析

6.6 本章小结

第七章 全文总结与展望

7.1 全文总结

7.2 后续工作展望

致谢

参考文献

攻读博士学位期间取得的成果