论文部分内容阅读
命题逻辑和一阶逻辑是逻辑学中的基本问题,也是计算机科学领域的核心问题。在推理系统中命题是命题逻辑公式的最小单位,一阶逻辑可以看作是命题逻辑的扩展,一阶逻辑增加了谓词和量化,是经典的谓词逻辑。SAT问题是布尔可满足性问题(Satisfiability Problem,SAT)的简称。SAT问题求解(SAT Solving)和一阶逻辑自动定理证明(Auto Theorem Proving,ATP)广泛应用于自然科学和社会科学的各个领域中,如数学定理的证明、通信协议的可靠性验证、集成电路的可靠性验证、程序自动生成以及程序测试例的自动生成、程序的形式化验证、智能规划、知识编译、密码的安全可靠性分析、法律法规的无歧义性分析验证等问题均可转换为SAT问题进行求解,同样一些内容也可转化为一阶逻辑定理证明问题进行证明。因此,研究SAT问题求解和一阶逻辑定理证明相关的理论与方法具有很高的理论意义和现实应用价值。并行算法能够有效的提高命题逻辑求解器和一阶逻辑定理证明系统的效率,基于此,本课题在命题逻辑并行求解算法和一阶逻辑定理证明中的并行算法方面展开研究。在命题逻辑方面研究命题逻辑并行求解的相关技术,在一阶逻辑方面借鉴命题逻辑并行求解方面的相关技术,并基于徐扬教授提出的基于矛盾体分离的多元协同动态自动演绎推理理论,设计和实现了针对一阶逻辑定理证明的基于矛盾体分离的多元协同动态自动演绎推理逆向演绎并行系统。提出了基于OpenMP的并行混合遗传算法框架,该算法框架将遗传算法与局部搜索算法有机结合用以求解3-SAT问题,充分利用了局部搜索算法的寻找局部最优解的能力和遗传算法的全局搜索能力。与此同时,有限的局部搜索迭代和灾变操作能够防止陷入局部最优,而对选择操作的算法改进则提高了遗传算法的运行效率。在OpenMP并行编程框架下,利用编译制导语句将混合遗传算法并行化,则充分利用了计算机的计算资源,通过对国际SAT问题库SATLib中的测试例进行测试发现,该算法框架与同类算法相比,提高了3-SAT问题的求解效率和成功率。针对硬件并行加速求解SAT问题,设计和改进了基于GPU的SAT问题求解算法,改进了GPU核函数的计算过程,设计了相应的数据结构,以便以位运算的方式完成BCP过程在GPU上的实现,同时位运算有效降低了核函数的分支数,提高了GPU的运行效率。针对现有的子句评估算法描述子句特征比较单一,保留的学习子句质量不高的问题。提出了基于频次与LBD混合的子句评估策略。在并行求解器的周期性删除学习子句模块替换原有的子句评估方式,同时在并行算法的子句共享模块应用该混合评估算法形成新的子句分享策略。实验结果表明,应用了混合评估算法的求解器求解能力均比原版本要高,与Syrup和abcd-SAT_P结合的版本求解出了原版未能求解出的43个问题。研究了基于矛盾体分离的多元协同动态自动演绎推理理论,在基于矛盾体分离的多元协同动态自动演绎推理理论框架下,提出了基于回溯的演绎路径控制算法,设计实现了基于矛盾体分离的多元协同动态自动演绎推理逆向演绎并行系统,实现了一阶逻辑问题真正意义上的并行划分演绎推理证明。从实验角度证明了基于矛盾体分离的多元协同动态自动演绎推理理论以及矛盾体分离的多元协同动态自动演绎推理逆向演绎理论的优越性。