论文部分内容阅读
基于模型诊断(Model-Based Diagnosis,MBD)是在人工智能领域发展中的一个重要研究方向。最初,模型诊断主要应用于电子电路故障的静态诊断,近年来,动态诊断逐步应用于大型软件验证、航天器安全性、通讯网络等领域,诊断问题已经成为理论研究与技术应用的双重焦点。目前,MaxSAT(Maximum Satisfiability)求解器是解决基于模型诊断问题的主要方法之一。MaxSAT问题是SAT问题的优化设计,目前,MaxSAT求解器包括完备MaxSAT求解器和不完备求解器,完备求解器能够在有效的时间内获得一个问题的最优解,不完备求解器能够在一定时间内返回一个近似最优解。带权重的MaxSAT和(不带权重的)PMS(Partial Maximum Satisfiability)是MaxSAT问题的两个重要的泛化版本,其中,PMS在网络路由调度问题、故障定位问题、制定时间表问题、组合拍卖、PGA路由等问题已经得到很好的应用,其子句用硬子句和软子句区分的形式使得编码模型诊断问题更加方便。目前,诊断问题已编码为PMS问题成为MaxSAT求解竞赛的实例。基于上述背景,本文研究内容如下:本文提出结合结构特征求解诊断问题的PMS求解算法SCPMS算法。该算法中提出了硬阻塞变量、软阻塞变量和结构特征明显子句集等概念,通过将结构特征明显子句集分为两部分,然后依据单元传播求解得到当前解对应的硬阻塞变量及其相关的软阻塞变量。算法在对子句集中的一部分子句进行单元传播时,然后判断该部分子句集的变量赋值是否与另一部分子句集的变量赋值有冲突,若有冲突,则直接得到软阻塞变量的赋值,从而有效缩小了待求解问题的求解空间;若不存在冲突,则继续在当前解对应的搜索空间中进行局部搜索,不会改变局部搜索算法在某些结构特征不明显的子句集求解的效率。在标准工业诊断实例上的实验结果表明,与DistUP算法和DeciDist算法相比,SCPMS算法较大程度地提高了求解效率。此外,本文针对DeciDist算法和SATLike算法中对硬单元子句和软单元子句的传播顺序不佳引起求解效率低下的问题,在对硬单元子句代表着诊断系统中的输入和输出观测的结构特征深入研究基础上,提出一种更适合于求解模型诊断类问题的基于冲突延迟传播的局部搜索方法CWPMS算法。该算法在单元传播过程中执行软单元子句延迟传播和冲突延迟传播机制。对硬单元子句优先传播时,执行软单元子句延迟传播机制。在硬单元子句传播后,当遇到冲突时采用冲突延迟传播机制,进而避免了冲突变量分配了错误值而引起的效率低下问题。在MBD标淮测试用例的实验结果表明,在300s的求解时间内,与SATLike算法相比,CWPMS算法求得的不满足软子句个数有较大程度地减少,提高了求解效率。以上的方法从两个不同角度出发对用Partial MaxSAT求解器求解模型诊断问题做了改进,提高了部分求解器求解诊断问题的求解效果。