2类数列问题循环不变式开发策略研究与应用

该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不变式,由此得到了2类数列问题循环不变式的统一开发策略.以二叉树的形态数问题和阶梯问题为例,利用所提策略开发循环不变式,并基于循环不变式展示了这2类数列问题算法程序的形式化推导过程.     

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.     

二叉树排序非递归算法推导及形式化证明

非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.     

图搜索问题算法推导及形式化证明

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.     

3个变形背包问题的形式化推导

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用.     

基于Web Service和多媒体数据库技术的PAR方法在线自学系统的设计与实现

设计并实现了一个PAR方法的在线自学系统.利用Web服务(Web Service)和多媒体数据库技术,将使用PAR方法开发算法程序设计的基本概念、算法设计语言Radl、抽象程序设计语言Apla以及设计和推导算法程序的方法学形象生动地呈现给学习者.最后介绍了利用算法程序设计支撑平台生成可执行算法程序的过程,以及该算法程序运行产生的结果.     

新算法程序的开发初探

算法程序是用可执行程序设计语言或抽象程序设计语言描述的算法，开发正确，高效率的算法是计算机科学的核心，为了提高算法程序的可聿性和生广效率，人们正在追求算法程序开发的形式化和自动化。     

模型驱动的Dafny程序形式化生成与自动验证

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法; 然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式; 最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.     

中国象棋计算机博弈系统评估函数的自适应遗传算法实现

使用自适应遗传算法解决中国象棋计算机博弈问题.将博弈问题分解为搜索引擎、走法生成、评估函数和开局库四大模块,然后将自适应遗传算法引入到评估函数中,通过锦标赛算法对评估函数中的参数组合进行自动调整和优化.设计并开发了基于上述方法的离线自学习系统,实验结果证明提高了程序的棋力.     

PLC程序形式化的设计与验证

从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.     

一个组合恒等式的证明和应用

分别用复变函数论、组合论和图论三种方法证明了 与数\,$n^{n-2}$\,的组合计数问题相关的一个组合恒等式, 并给出该恒等式在图论、超平面配置等一些组合问题上的应用.     

完全i部图N［(X1,X2,…,Xi),k］计数公式

采用组合卷积公式方法,研究图的S(n)-因子的计数问题.首先获得完全2-部图的恰有k个分支的S(n)-因子的计数公式,并用同样方法获得完全i-部图的恰有k个分支的S(n)-因子的计数公式,从而给出完全i-部图的所有因子数计数公式.进一步研究了完全i-部图的组合恒等式,并通过组合计算技巧,获得了完全i-部图、完全2-部图和完全3-部图的组合恒等武.该研究对图论及组合学具有理论和应用价值.     

复杂算法程序的规范证明和形式推导

能否实现复杂算法程序的规范证明和形式推导是检验某种形式化方法有无生命力的重要标志。本文介绍了这一领域的研究现状,重点综述了作者近年来提出的复杂算法程序形式化技术,以典型实例说明了使用这些技术的方法。     

An adaptive ant colony system algorithm for continuous-space optimization problems

Ant colony algorithms comprise a novel category of evolutionary computation methods for optimization problems, especially for sequencing-type combinatorial optimization problems. An adaptive ant colony algorithm is proposed in this paper to tackle continuous-space optimization problems, using a new objective-function-based heuristic pheromone assignment approach for pheromone update to filtrate solution candidates. Global optimal solutions can be reached more rapidly by self-adjusting the path searching behaviors of the ants according to objective values. The performance of the proposed algorithm is compared with a basic ant colony algorithm and a Square Quadratic Programming approach in solving two benchmark problems with multiple extremes. The results indicated that the efficiency and reliability of the proposed algorithm were greatly improved.     

《组合数学》实践性教学研究

《组合数学》是理论和应用结合很强的一门学科。多年的教学经历发现,很多学生并不明白《组合数学》和其他应用学科的关系。文中介绍了教学过程中通过一些典型的实践性问题的解决,使学生能够理解并掌握怎样用组合数学去解决其他学科的问题,同时一些组合数学的问题怎样用其他学科的方法去解决。教学效果表明,文中的实践性教学尝试是成功的。     

Fitness Landscape Analysis for Optimum Multiuser Detection Problem

Optimum multiuser detection （OMD） for CDMA systems is an NP-complete combinatorial optimization problem. Fitness landscape has been proven to be very useful for understanding the behavior of combinatorial optimization algorithms and can help in predicting their performance. This paper analyzes the statistic properties of the fitness landscape of the OMD problem by performing autocorrelation analysis, fitness distance correlation test and epistasis measure. The analysis results explain why some random search algorithms are effective methods for OMD problem and give hints how to design more efficient randomized search heuristic algorithms for OMD.     

基于局部填充函数的混合优化算法的改进

填充函数算法是求解全局优化问题的常用算法,其应用效果依赖于如何合理地选择算法参数。为了方便地选择参数,该文提出了局部填充函数的概念,并讨论基于局部填充函数的混合优化算法的改进策略。对于给定的参数,混合优化算法寻找一个包含极小点的区域,使得所构造的函数在该区域上满足局部填充函数的定义,从而利用局部填充函数的性质简化寻优过程,减少优化过程中参数调整的次数和难度,提高算法的效率和稳定性。此外,针对填充函数算法研究中简单盆存在性问题,该文给出了一个实例,说明二次连续可微的函数在一定条件下其孤立极小点附近可以不存在简单盆。     

从完全基因组出发建立原核生物亲缘关系和分类系统时遇到的数学问题

我们课题组近10年所发展的组分矢量(CVTree)方法,已经成为从完全基因组出发而不使用序列联配来构建细菌亲缘关系的有效手段.在整个生物分类学日益后继乏人的背景下,组分矢量(CVTree)方法伴随着基因组时代的发展,成为人人可以方便使用的微生物分类的定义性工具.本综述不讨论CVTree的生物学结果,而着重从非线性科学的角度,介绍我们在研究过程中所提出和解决的数学问题.这将涉及组合学、图论、形式语言学等离散数学的篇章.我们特别希望,本文所列举的一些尚未解决的数学问题能引发新的研究工作,使CVTree方法的理论基础更为坚实.     

基于局部填充函数的混合优化算法的改进

填充函数算法是求解全局优化问题的常用算法,其应用效果依赖于如何合理地选择算法参数。为了方便地选择参数,该文提出了局部填充函数的概念,讨论了基于局部填充函数的混合优化算法的改进策略。对于给定的参数,混合优化算法寻找一个包含极小点的区域,使得所构造的函数在该区域上满足局部填充函数的定义,从而利用局部填充函数的性质简化寻优过程,减少优化过程中参数调整的次数和难度,提高算法的效率和稳定性。此外,针对填充函数算法研究中简单盆存在性问题,该文给出了一个实例,说明二次连续可微的函数在一定条件下其孤立极小点附近可以不存在简单盆。     

基于偏序对改进蝙蝠算法的旅行商问题研究

作为一种新兴的群智能启发式算法,蝙蝠算法近年来被广泛用于求解离散、连续、及组合优化问题。针对典型组合优化问题中的旅行商问题,本文提出一种基于偏序对改进的蝙蝠算法用于求解离散型旅行商问题。通过对蝙蝠速度、位置的更新,使算法具有更强的适用性。本文对16个标准TSP问题进行测试与对比分析以验证算法有效性。实验结果表明,本文提出的偏序对蝙蝠算法在大多数实例中均优于其他算法。