基于混合蚁群遗传算法的SAT问题求解

根据SAT问题的特点,通过分析传统蚁群算法和遗传算法在求解SAT问题上的不足,提出一种基于混合蚁群遗传算法的SAT问题求解方法。给出一种新的初始解的生成方式;在迭代过程中,根据较优解的累积信息提出进化算子;利用当前得到的最优解,通过改变不满足子句中文字的取值,增加变异算子。最后选取标准测试集中的20个实例对算法进行测试,实验结果表明:改进后的算法通常仅通过较少次数的迭代就能找到解,能够有效避免蚁群算法和遗传算法过早收敛的缺点,具有较强的寻优能力。     

基于AC与LmaxRPC的自适应约束传播求解算法

在现有自适应约束求解方法基础上,提出一种新的自适应约束传播求解算法ADAPTAC-LmaxRPC.该算法能根据约束的不同特性,在传播能力强但开销高的LmaxRPC与传播能力弱却开销低的AC之间自适应地切换进行约束传播.多个Benchmark实例类上的测试实验数据表明,ADAPTAC-LmaxRPC算法有效地平衡了求解效率和算法开销之间的矛盾,大幅度提高了约束求解的效率.     

一种改进的和声搜索算法及其应用

为了克服和声搜索算法(Harmony Search Algorithm,HSA)方向性差和收敛速度慢的缺陷,提出一种新的和声搜索算法。新算法设置一个主种群和多个子种群,主种群和子种群分别采用全局差分HSA和局部差分HSA进行优化,所有种群通过排序循环划分方法进行协同优化。随机3—SAT测试实例和三个典型Benchmark函数上的实验表明,新算法是可行的、有效的。     

心理学在船舶安全管理中的应用

本文分析了船舶失事势船员常见的不良心理状况,介绍了可导致人保持正常心理的几种激励理论,并提出了解决船员心理问题的具体办法。     

一种形式化的构件模型框架

构件理论在软件工程领域正扮演着越来越重要的角色。为了规范化地描述和设计构件 ,提出了一种形式化的构件模型框架 ,利用偏序事件多集来表示构件的行为模式 ,取代了常用的形式语言表示法 ,使顺序进程控制的构件和并发控制的构件能够在该框架下得到一致的处理。论文关于构件模型、任务合同及系统模型的概念 ,结合构件完备性、服务可满足性和系统一致性的检验方法 ,可以直接被用于设计构件支撑环境的仿真算法。     

浅谈初级指挥院校学历教育如何优先满足第一任职需要

武警部队初级指挥院校作为武警部队生长干部的重要培训基地,直接担负着为基层培养和输送初级指挥警官的教学任务。多年来,这些院校始终贴近部队实际,把优先满足学员第一任职需要作为重要的办学指导思想,着力培养学员的第一任职能力方面,进行了积极的、卓有成效的探索和实践。进行军事职业教育,培养学员第一任职能力,是初级指挥院校的传统优势,也是未来发展的强项。     

命题公式真值表的生成与公式类型的机械判定

在文[1]的基础上,给出了命题逻辑中任一命题公式的真值表的生成算法与命题公式类型的判定算法,实现了利用计算机对有限多个命题公式的真值表的直接计算和输出,以及对一个命题公式是重言式、矛盾式或可满足式的机械判定.     

提供优质服务 构建和谐高校图书馆

本文论述做好信息资源的建设,提供优质的信息服务,满足读者的需求达到读者的满意,构建和谐高校图书馆。     

量化单一带标公式的消解

在引入量化单一带标公式的概念后,给出其消解算法,并证明该消解算法是健全的和拒绝性完备的。因此该算法可用于对量化单一带标公式进行理论上的研究,同时也可用于在实际应用中解决这类公式的可满足性问题。最后,根据消解算法,得出一个可以在多项式时间内判定可满足性的量化单一带标公式的子类。     

一个改进的通用成卷模型及其智能算法

针对现有试题库系统普遍存在的“成卷结果难以使教师从主观上感觉满意”的问题,对试卷的“可用性”进行了分析,增加了“知识点不重复”、“题型、内容及难度分布均匀”、“最近试卷中的试题不重复”等可用性约束,改进了现有的成卷模型．提出以“可满足度”为启发信息的智能成卷算法．通过对高等教育出版社发行的多门试题库的实际使用表明,该模型对理、工、医等多种学科具有通用性,并且完全消除了知识点的重复,减少了成卷误差和试题分布不均匀程度．