摘要：#SAT问题是SAT问题的扩展,需要计算出给定命题公式集合的模型个数.通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有模型计数问题求解方法的一种补方法.证明了该方法的完备性和有效性,设计了基于扩展规则的#SAT求解系统:JLU-ERWMC.实验结果表明,JLU-ERWMC在有些问题中优于目前最为高效的#SAT问题求解系统.

摘要：不确定环境下的智能规划问题往往假设世界状态的转移概率是确切可知的,然而规划建模专家有时只能在信息不完备的条件下进行建模,从而只能通过猜测或者不完全统计的方法来获取不完备的有关状态转移不确定性的定量信息,有时甚至只能获取相关的定性信息.在2004年概率规划比赛冠军LAO系统的基础上设计了JLU-RLAO系统和JLU-QLAO系统.它们可以在无法获得精确的状态转移概率条件下,依然保证规划求解的健壮性.实验结果表明,JLU-RLAO系统和JLU-QLAO系统可以快速高效地解决上述不确定智能规划问题.

摘要：为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域,对不可满足子式进行了相关研究.对当前不可满足子式的主要相关算法进行了概述评论、分类归纳,并从计算复杂性角度介绍了其子类、参数复杂性以及QBF中的极小不可满足子式.总结了近10年来不可满足子式的理论与算法,讨论了不可满足子式的未来研究发展方向.研究有利于进一步发现不可满足的根本原因,从而进行有针对性地改进,并对相关人员的研究提供帮助.

摘要：在基于扩展规则的知识编译算法的基础上提出了2种启发式策略:MCN策略和MO策略.MCN策略和MO策略利用子句集的信息分别选择相应子句和变量,减少扩展规则的使用次数,进而降低知识编译后目标子句集的规模.在此基础上,设计并实现了MCN_KCER,MO_KCER和MCN_MO_KCER算法.实验结果表明:2种启发式策略都可以大幅度减小编译后的子句集规模,同时使用它们的效果更为明显,经过编译后得到的子句集规模是原算法的1/3～1/39,从而大幅度提高之后的在线推理阶段的效率.

摘要：提出了一种结合增量与启发式搜索的多目标问题处理方法,设计并实现了一个基于路径扩展方法的多目标增量启发式搜索系统.当问题搜索图中边的权重发生改变或添加删除节点时,该系统通过对搜索现场进行实时的更新,部分利用先前搜索保留的信息,从更新后的状态开始求解新的问题,从而提高了重搜索的效率.对gridworld标准测试样例进行了大量的系统测试,实验结果表明:结合增量与启发式搜索的处理方法能够有效地解决状态格局不断变化的一系列相似的多目标最短路径问题.

摘要：#SMT问题是SMT问题的扩展,它需要计算一阶逻辑公式F所有可满足解的个数.目前,该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用,设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因,设计了一种求解较大规模#SMT实例的近似求解器——Vol Compute With Local Search.它在现有的#SMT精确求解算法的基础上加入差分进化算法,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.另外,从理论上证明了Vol Compute With Local Search求解器可以得到精确解的下界,使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明:Vol Compute With Local Search求解器是稳定的、具有快速的求解能力,并在高维问题上具有很好的表现.

摘要：为支持"玉兔号"巡视器完成对月面较大空间范围的科学探测,对动态任务进行快速规划,提出了一种基于人工智能领域智能规划技术的自动化任务规划方法。提出了行为持续时间和行为效果动态确定的时态规划模型(TP^(DD&DE)),设计了描述TP^(DD&DE)问题的规划领域定义语言PDDL——PDDL^(DD&DE),以及针对TP^(DD&DE)问题的启发式规划算法,运用Landmark知识分析规划问题结构,从而设计了合理反映动作前提评估顺序的启发函数。在嫦娥三号任务中,本文方法支撑"玉兔号"巡视器圆满完成了预期的科学探测任务。

摘要：视频跟踪是计算机视觉的重要组成部分,可在智能交通、医疗诊断等实际应用中发挥重要作用.近年来,相关滤波器凭借精度高、速度快的优势,逐步发展为视频跟踪方法的主要研究方向之一,可以很好地处理多种视频跟踪难题.随着基于相关滤波器的视频跟踪系列方法被相继提出,算法设计趋于完善,跟踪效果也趋于精准.本文从不同角度总结了多种具有代表性的相关滤波跟踪方法,分析了各种方法的发展进程,并预测了未来可能的发展方向.

摘要：提出了一种启发式调查传播算法,并基于该算法设计了一种QBF(quantified Boolean formulae)求解器——HSPQBF(heuristic survey propagation algorithm for solving QBF)系统.它将Survey Propagation信息传递方法应用到QBF求解问题中.利用Survey Propagation作为启发式引导DPLL(Davis,Putnam,Logemann and Loveland)算法,选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,HSPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而能够提高QBF问题的求解效率.实验结果表明,HSPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值.

摘要：根据动作组件诱发关系的存在和抵制计算的必要性,提出一个计算松弛规划解的新方法——延迟部分推理.该方法在考虑动作删除效果的假定下,构造不包含任何互斥关系的组件规划图,通过定义"松弛诱发"关系预测后续规划过程中可能出现的组件诱发现象,在松弛规划解提取阶段判断动作组件间的"松弛诱发"关系并选择抵制动作避免可能发生的消极作用.基于延迟部分推理方法定义了新的启发式函数和剪枝策略,设计了规划系统FFc并在多个国际通用的测试域上进行实验.结果表明,FFc较之Fast-Forward在求解效率和求解质量方面都有显著的提高.