几何定理机器证明并行算法研究

论文摘要

定理机器证明的研究，在理论和实践上都具有重要的意义。当前，机器证明的理论研究进入低潮时期，自20世纪末以来，国外研究人员尝试将并行计算技术引入到符号计算的一些关键计算问题当中，以求获得更高的计算效率，而在国内，这方面的研究还处于起步阶段。 本文遵循上述研究思路，将几何定理机器证明和并行计算结合起来考虑，主要探讨前推法、数值并行法的并行化算法，并在MPICH构建的并行计算试验环境下进行实现和测试。本文工作主要集中在以下几个方面： （1）介绍了几何定理机器证明和并行计算的基本理论，对几种不同的并行编程模式进行分析。在此基础上，用MPICH构建并行计算试验环境，并实测了该环境点对点和组通信状态下的MPI性能，为下面的工作和算法优化打下基础。 （2）利用任务／通道模型，完成了前推法并行化的任务划分和通信组织，并给出MPI下程序实现的算法框架，在算法实现中还探讨了提高前推法效率的一些关键问题。分析任务调度算法实现，给出了执行时间表达式。 （3）从任务／通道模型出发，分析数值并行法的任务划分和通信组织，并给出了MPI环境下程序实现的算法框架。对动态和静态的任务调度算法进行分析，通过对其时间表达式的比较，从而选择合适的任务调度算法。 （4）分析了吴方法中的关键算法—多项式特征列算法，给出特征列算法并行化的方案。探讨了多项式并行乘法和大整数并行乘法在MPI环境下的实现，对算法进行了简单分析。 （5）在大量实验数据基础上，通过对加速比、并行效率、Karp-Flatt量度等评价指标的分析，对算法的实际效率做出评价。 本文从理论和实践上探讨了定理机器证明一些方法的并行可行性，但所设计的前推并行推理算法在效率上不尽如人意，还需要进一步挖掘其并行性以提高效率，同时改进算法以适应异构的分布式计算平台。

论文目录

• 第一章 引言
• 1.1 几何定理机器证明现状
• 1.2 并行系统和并行算法研究现状
• 1.3 本文研究目标和内容
• 1.4 论文的组织和安排
• 第二章 理论基础与概念描述
• 2.1 几何定理机器证明方法介绍
• 2.1.1 几何信息搜索方法
• 2.1.2 数值并行法
• 2.1.3 吴方法
• 2.2 并行计算理论简介
• 2.2.1 并行计算机系统
• 2.2.2 并行编程模型
• 2.2.3 并行算法设计
• 2.2.4 并行算法性能量度
• 第三章 并行编程接口MPI简介
• 3.1 MPI的目的
• 3.2 MPI新发展
• 3.3 当前 MPI-2的实现
• 3.4 MPI性能研究
• 3.4.1 基于消息传递的并行程序性能模型
• 3.4.2 点对点状态性能研究
• 3.4.3 组通信状态性能研究
• 第四章 证明器的 MPI环境实现
• 4.1 前推法的 MPI并行实现
• 4.1.1 并行策略分析
• 4.1.2 程序设计
• 4.1.3 任务调度策略
• 4.1.4 算法复杂度分析
• 4.2 数值并行法的 MPI并行实现
• 4.2.1 并行策略分析
• 4.2.2 任务调度策略
• 4.2.3 程序设计
• 4.3 并行特征列算法初探
• 4.3.1 大整数并行乘法
• 4.3.2 多变元多项式并行乘法
• 第五章 实例与分析
• 5.1 前推法算法评价
• 5.2 数值并行法评价
• 第六章 结论和展望
• 6.1 主要研究工作回顾
• 6.2 研究成果和结论
• 6.3 进一步工作的方向
• 参考文献
• 致谢
• 发表文章目录
• 附录1
• 附录2
• 附录3
• 附录4