mis管理实践论文范文

我得博士老师的论文

信息管理学院 课程论文

班 级：＿＿＿＿＿＿＿ 学 号：＿＿＿＿＿＿＿ 姓 名：＿＿＿＿＿＿＿ 专 业：＿＿＿＿＿＿＿ 指导教师：＿＿＿＿＿＿＿

信息管理学院 信息资源管理系

二○○ 年 月 日

我得博士老师的论文

（范文）MPI环境下的定理并行自动推理

姓名: 学号:

[摘要] 本文将几何定理机器证明和并行计算结合起来考虑，尝试用并行计算方法来提高传统定理证明算法效率，探讨了前推法、数值并行法的并行算法，分析了两种定理证明算法在消息传递编程模型下的任务划分、通信组织、任务调度等问题，并用MPICH2实现了这两种并行算法，对算法的并行性能指标进行了测试，测试数据表明，两种并行算法在基于MPI-2的并行计算环境下，能很好地发挥并行计算的优势，有效缩短构造性几何命题机器证明的时间。

关键词: 前向推理，并行算法，数值并行法，性能量度，定理证明

The Parallel Algorithms for Mechanical Geometry Theorem Proving

Abstract The paper considers combining the mechanical geometry theorem proving with the parallel computation method, attempts the parallel computation method to improve the efficiency of traditional theorem proving algorithms, discusses the parallel algorithms of the forward reasoning and the numerical verification method, analyzes the partitioning, communication and the task-scheduling algorithm with the message-passing programming model, implements the algorithms with MPICH 2, and then tests on the efficiency of the algorithms with parallel performance metrics. The result shows that the parallel algorithms could take advantage of parallel computation, and obviously reduce the proving time of constructive geometric theorems.

Key words：forward reasoning; parallel algorithm; parallel numerical method; performance metrics; theorem proving

1 前言

人工智能与自动推理技术的应用十分广泛，几何定理机器证明是其中一个重要的分支。在实际运用中，对很多复杂度较高的问题，现有的算法在合理的时间内还不能解决。20世纪末以来，国外的一些研究人员已经开始尝试将并行计算技术引入到符号计算当中，以解决一些高复杂度的问题[1]。本文将几何定理机器证明和并行计算结合起来考虑，主要探讨前推法、数值并行法的并行化算法，并在消息传递接口MPI-2的一个具体实现即MPICH 2所构建的并行计算环境下进行实现和测试。

2 理论背景

前推法是一种基于规则的推理方法，类似于人的解题过程。前推法有两个特点：(1) 能够产生传统形式的可读证明；(2) 无论结论是否能够被推出，都能产生大量有用信息。但是，当前推达到推理不动点仍未推出命题结论，并且不能断定命题不成立，需要用其他方法辅助推理，如添加辅助线、使用反证法等。实际上，可以用代数的方法(吴方法、数值验证法等)对命题的真伪做预先判定。数值验证法的基本思想是：要肯定或否定一条初等几何命题，只要检验若干个数值实例即可。与吴方法等代数方法相比，该方法用数值计算代替符号计算以减少解题难度，是很有特色的一种辅助方法。

文献[2-3]介绍了前推法的基本理论，关于数值验证法的具体理论阐述，可参看文献[4-5]。

3 并行算法设计

3.1 并行前推法

并行前推法程序从文件中读入一个几何命题，将题设条件写入初始信息库，不断将规则库中的规则应用于信息库，直到无法产生新的几何信息，然后检查信息库中是否有命题结论，若存在，则输出可读证明到文件中，否则，打印命题证明失败的信息。

(1) 任务划分。对各子步骤的数据依赖关系作分析，结果如图1所示。

我得博士老师的论文

图1 并行化后的数据依赖图

于是，每个操作可以映射为一个原始任务，每个原始任务和2个数据单元(条件信息组+规则)相关联。比较好的数据关联策略是所有计算节点采用同样的规则集，不同的条件信息组进入节点进行匹配，这是条件组层次的并行，其并行粒度小，可扩展性也更好。

由于任务的数目在编译时无法确定，各个任务之间不需要通信，完成不同任务所花费的时间也不尽相同，所以任务的映射应该在运行期完成，本文选择Master-Slave模式[6-7]实现算法，用Master进程进行I/O操作和任务分发。

(2) 通信组织。本文采用任务/通道模型[7]来描述算法中的通信情况。最初的通信由Slave进程开始，它发送一个“就绪”消息给Master进程，Master进程用题设条件构成初始信息库，向所有Slave进程广播该信息库，然后开始构造和分发规则匹配任务。在图2中，细虚线箭头表示广播规则的通道，粗虚线箭头表示信息库广播和匹配任务分发的通道，点划线箭头表示新信息回送给Master的通道。

图2 前推法任务/通道图

在Slave进程进行一轮规则匹配后，各个Slave进程产生的新信息是不一样的，需要进行调整以保证本地

和全局信息库的一致性。显然，Master进程收集完新信息后，只需向各Slave进程广播一次即可。

(3) 任务调度和复杂度分析 Master-Slave程序模式采用的是一种动态的任务分配策略，为了减少进程间额外的通信开销，Master进程在给Slave进程分配数据的时候，使用按组分配任务的策略，每次分配k个任务。k的具体数值受多个因素的影响，需要进一步分析。

先前的设计中，构造匹配任务被设计成串行任务。本文采用流水线法进行改进：当Slave处理已有的匹配任务时，Master进程可以同时开始构造新的匹配任务。但是需要注意的是，如果当前信息库中的信息都已经用来产生匹配任务，那么Master进程停止匹配任务的构造，等待信息库的更新。

本文仅粗略分析算法主体部分(忽略文件I/O时间)执行时间的表达式。由于采用了流水线方法，Master进程上进行的匹配任务的串行时间只需要计算到生成第一批任务的时间。

设N为一次证明产生的匹配任务总数，P为处理器数目，k为每个处理器完成一轮推理的任务数目， 为

t0为Master进程产生一个匹配任务的时间，t1为Slave进程完成一次规则匹配的时间(包消息传递的延迟时间，

括检验新信息)。在一轮推理中，要进行信息库分发和结论信息收集2次广播通信。由于在MPI中，实现广播

[8]

通信的算法的通信步数为 lbP ，所以总的开销为2 lbP ，还要进行一次任务的分发，其开销为 P，所以算法的执行时间为：

我得博士老师的论文

(kP)t0

N kP

(kt1 2 lbP P) kP

N kP

为循环推理的次数；kP

kt1为单个处理器完成每一轮规则匹配的时间(完成k个任务)。实际上，对每一个几何命题，N是不能预先确定的，并且，虽然把每次消息传递的延迟统一处理了，但还是要受信息库以及推理结果信息大小的影响，所以上述表达式只能作为复杂度分析的参考，算法效率的分析应该以实际运行指标为重点。从上式还能够

式中 (kP)t0为Master产生第一批匹配任务的时间；N kP是剩余的匹配任务；看出，当k

k值确定问题。

3.2 并行数值验证算法

并行数值验证程序从文件中读入一个几何 …… 此处隐藏：7495字，全部文档内容请下载后查看。喜欢就下载吧 ……