计算机学科研究生科研基础的建立模式

以研究生科研基础的建立模式为着眼点,分析多年来试行的培养机制和协作机制,提出研究生科研基础模式建立的方法和几个阶段,以促进对研究生科研潜质的开发。     

peC语言的部分求值器及在编译器测试中的应用

部分求值技术在程序优化及软件自动生成等方面,有着极为重要的作用.本文将部分求值技术应用到编译器测试中.为此,设计了一个C语言的子集peC语言,给出了该语言的部分求值策略的形式化描述,实现了peC语言的部分求值器,设计了基于部分求值技术的编译器测试框架.通过实验,本文的方法可以检测出大部分之前的其它的方法发现的GCC、LLVM编译器中的错误,此外还发现了其它方法不能发现的错误,表明将部分求值技术应用到编译器测试中是有效的.     

EPCCL理论的求交知识编译算法

超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以EPCCL（each pair of clauses contains complementary literals）理论的形式保存.基于超扩展规则的性质,本文提出了一种新的EPCCL理论编译算法：求交知识编译算法IKCHER（intersection approach to knowledge compilation based on hyper extension rule）,该算法适合难解类SAT问题的知识编译,同时是一种可并行的知识编译算法.本文还研究了如何实现多个EPCCL理论的求交操作,证明了EPCCL理论的求交过程是可并行执行的,并设计了相应并行求交算法PIAE（parellel intersection of any number of EPCCL）.通过对输入EPCCL理论对应普通子句集的利用,设计了一种高效的并行求交算法imp-PIAE（improvement of PIAE）.基于上述算法本文还设计了两个并行知识编译算法P-IKCHER（IKCHER with PIAE）和impP-IKCHER（IKCHER withimp-PIAE）,分别采用PIAE并行合并算法和imp-PUAE并行合并算法.最后,通过实验验证了大部分情况下IKCHER算法的编译质量是目前为止所有EPCCL理论编译器中最优的,P-IKCHER算法所使用的合并策略并没有起到加速的效果,反而使得编译效率和编译质量有所下降,而impP-IKCHER算法提高了IKCHER算法的编译效率,四核并行下最高可提高两倍.     

一种1553B总线远程终端的即插即用的设计

随着航天技术的不断发展,研制即插即用、低成本、小型化的卫星渐渐成为一种趋势,我国的星上数据管理系统使用1553B总线连接各个有数据交换需求的计算机与分系统,这些计算机与分系统也就成为1553B总线的远程终端;为了设计即插即用的1553B远程终端,对电子数据表单(Electronic data sheet,EDS)、龙芯1F中的1533B简易终端进行了研究,分析了电子数据表单的设计方法和使用方式,提出了应用EDS、1553B通信EDS的设计方法;分析了1553B简易终端对龙芯1F中测控接口的访问控制方式,在龙芯1F中添加了一个SPA(Space Plug-and-play Avionics)接口,与1553B简易终端联合使用,当龙芯1F作为1553B总线上的一个终端设备时,具有了即插即用的特征;由此说明1553B远程终端是可以实现即插即用的,同时把即插即用这一新的设计理念带入星载数据系统的设计中。     

基于扩展规则的启发式#SAT求解算法

#SAT在人工智能领域取得了广泛应用,很多现实问题可以规约成#SAT进行求解,得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究,发现选择规约子句的顺序对极大项空间的大小有着较大的影响,因此提出两种加速#SAT求解的启发式策略：MW和LC&MW.MW每次选择具有最大权值的子句作为规约子句;LC&MW每次选择最长子句作为规约子句,若最长子句存在多个,则在多个最长子句中选择具有最大权值的子句作为规约子句.利用MW策略设计了算法CER_MW,利用LC&MW策略设计了算法CER_LC&MW.实验结果表明,CER_MW和CER_LC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面,CER_MW和CER_LC&MW的求解速度是其他算法的1.4倍~100倍.在求解能力方面,CER_MW和CER_LC&MW在限定时间内可解的测试用例更多.     

基于多值表示的并行规划方法

Fast Downward规划系统是第四届国际规划竞赛的冠军.以高效的串行规划系统Fast Downward为基础,设计并实现了并行规划系统Parallel Downward.首先提出4个并行规划的相关定义;之后提出多值规划任务下动作互斥的定义、充要条件,并实现了动作互斥判断算法;在此基础上设计了候选并行动作集的生成算法;然后为提高系统求解质量重新设计了新的搜索控制策略;最后,给出剪枝策略来抑制并行规划状态空间的指数级膨胀.通过对国际规划竞赛测试问题的实验,Parallel Downward表现出良好的规划效率和规划质量,相比Sapa规划系统Parallel Downward具有较好的可扩展性.     

基于自动推理技术的智能规划方法

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.     

一种新的基于扩展规则的定理证明算法

基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法,首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时问和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.     

基于Conformant Fast-Forward规划系统的析取目标处理方法

将规划系统Conformant Fast-Forward从单目标规划扩展到基于析取目标的不确定规划,设计并实现了新的规划系统Conformant-FF-d.Conformant-FF-d的新功能主要包括:目标状态判断、可达性分析和启发函数.提出一种利用SAT技术进行目标状态判断的高效方法;提出析取目标条件下信念状态的可达性分析方法,有效地删除无法到达目标的信念状态,进而缩小了搜索空间的规模;设计了适用于析取目标的启发函数,有效地指导搜索算法向更有希望到达目标的方向进行.在国际规划竞赛的问题域上对Conformant-FF-d和先进的规划系统POND进行测试和对比分析,实验结果表明:ConformantFF-d的求解效率高而且具有较好的可扩展性.     

基于MACR和CAL启发式的求差知识编译算法

DKCHER算法是基于超扩展规则的求差知识编译算法.本文首先研究了DKCHER算法的执行流程,并定义了互补量的概念,然后设计了启发式策略MACR（maximum complementary amount of clauses with middle result）,用于动态选择与中间结果互补量最大的子句.针对互补展开过程,设计了动态启发式策略CAL（optimal sequence sorted by complementary amount of literals）,将互补展开中的文字按照与输入公式互补量的大小进行排序并展开.将上述两种启发式策略与DKCHER算法相结合,分别设计了MACR_DKCHER算法、CAL_DKCHER算法和MACR_CAL_DKCHER算法.实验结果表明,MACR启发式策略能够提升DKCHER算法的编译效率和编译质量,编译效率最高可提升9倍,编译质量最高可提升1.9倍;CAL启发式策略在子句数和变量数比值较大的实例上,能够提高DKCHER算法的编译效率,但会降低DKCHER算法的编译质量;MACR_CAL启发式最高可将DKCHER算法的编译效率提高12倍,但会导致DKCHER算法的编译质量有所降低.