论文部分内容阅读
模型诊断（Model-Based Diagnosis，MBD）问题是人工智能领域的重要研究方向之一，可追溯至1987年De Kleer、Williams和Reiter的具有重要性标志意义的工作。到目前为止，MBD问题已发展到利用多种不同的模型进行建模，如离散事件模型、定性模型、不完全因果模型和混合模型。并且其成果也成功应用到多个领域，如航天航空、汽车制造、电信网络、燃气轮机条件监测、软件验证、以及电路的诊断和故障排除。
基于一致性的组合电路MBD方法以逻辑公式形式对系统进行建模，旨在高效率获取所有诊断以及高质量的健康态。本文主要针对单观测诊断方法及其延伸而来的多观测诊断方法、健康态方法进行研究，以达到提高求解效率和求解质量的目的。主要内容如下：
1)结合SAT技术来解决MBD问题作为直接诊断方法的重要方式之一，因其求解特征，在解决MBD问题过程中还需其它结构的辅助以生成候选解空间，如集合枚举树，并利用SAT（Satisfiability）求解器来判断候选解是否为诊断。但该类方法存在对候选解空间的冗余解进行一致性检测的不足，因此，本文提出结合SAT的分组式诊断方法（Grouped Diagnosis，GD）实现电路元件的分组并剪枝这些冗余空间，以提高算法效率。该方法首先结合电路特征，利用单元传播规则获取故障输出，依据电路逻辑与故障输出将电路中元件进行分组。其次结合诊断问题和SAT求解过程的特征，给出非诊断定理和分组式诊断方法，并利用分组后的电路加速对集合枚举树无解空间的剪枝，进而提高算法求解效率。实验结果表明，针对获取所有极小子集诊断，在相同的诊断长度限制下，GD方法比目前最先进的结合集合枚举树的基于SAT的MBD方法求解效率更高。
2)MaxSAT（Maximal Satisfiability）技术也是用来解决MBD问题的高效方式之一，但其不需要额外的结构辅助，因此引出提高算法效率的另一种途径——对电路系统进行抽象，该方式可缩减问题规模。目前的抽象算法主要为基于分层抽象方法，该方法在抽象电路上得到顶层诊断（Top-Level Diagnosis，TLD），再对TLD进行迭代枚举替换操作，以得到所有的极小势诊断，但该方法的缺陷在于需要对拓展诊断逐一检查一致性，这个过程十分耗时。因此，本文给出一种结合MaxSAT的区域化抽象诊断方法（Zonal Diagnosis，ZD）。首先结合电路特征，提出新的抽象模型，将电路划分成不同的Zone，并利用MaxSAT求解器在由这些Zone构成的抽象电路上得到极小势抽象诊断。其次利用值传播特点提出了一种新的传播扩展方法，用于扩展极小势抽象诊断以有效地获得所有极小势诊断，从而避免检查一致性，提高求解效率。实验结果表明，针对获取所有极小势诊断，在相同的诊断数量限制下，ZD算法比目前最先进的基于分层抽象的算法求解时间更短，显著提高了算法效率。
3)健康态作为诊断算法求解质量的代表，该形式表示系统所有元件故障的可能性，在故障排除等问题中有十分重要的应用。健康态通过诊断列表及其分数计算而得，且不需要所有的诊断参与计算即可得到质量收敛的健康态，但不足之处在于该诊断列表中诊断均只解释一个观测，诊断的精确度较低，从而影响健康态质量。因此，本文设计一种结合多观测和差异度的提高健康态质量方法（Improve the Quality of Health State with Difference Degree，IHSD）来解决该问题，以获取更高质量的健康态。结合健康态计算时不需要所有诊断即可质量收敛的特征，该方法首先给出适应健康态计算的多观测MBD方法，利用多观测诊断方法对诊断进行整合，得到同时满足多观测的精确诊断。其次结合“差异度”概念对评分机制进行修改以对精确诊断进行评分，尽量提高精确诊断的分数以尽可能接近真实故障情况，从而提高健康态的质量。实验结果表明，设置相同的收敛参数，与目前最先进的计算健康态方法对比，IHSD算法显著提高了健康态的质量。
4)与单观测MBD方法相比，多观测MBD方法可对多个观测结果进行联合诊断以识别常见的故障位置，且该方法在程序故障定位等领域取得成功，针对基于一致性的组合电路多观测MBD问题，有学者给出两种完备方法，即诊断组合方法和碰集二元性方法。考虑到观测增量化的情况，诊断组合方法是合适的，但其在获取满足多观测的精确诊断过程中，无法完全避免非极小解情况的出现，仍需子集检测过程辅助，影响算法效率。因此，本文提出增量的多观测极小诊断方法（Incremental MBD with Multiple Observations，IMBDMO）。该方法首先给出极小子集精确诊断定理和诊断组合规则，确保精确诊断的子集极小性且避免子集检测过程，进而提高算法效率。其次实现观测增量化。实验结果表明，与目前最先进的诊断组合方法对比，IMBDMO算法显著提高了算法效率且在观测增量化情况下依然保证算法高效性。
基于一致性的组合电路MBD方法以逻辑公式形式对系统进行建模，旨在高效率获取所有诊断以及高质量的健康态。本文主要针对单观测诊断方法及其延伸而来的多观测诊断方法、健康态方法进行研究，以达到提高求解效率和求解质量的目的。主要内容如下：
1)结合SAT技术来解决MBD问题作为直接诊断方法的重要方式之一，因其求解特征，在解决MBD问题过程中还需其它结构的辅助以生成候选解空间，如集合枚举树，并利用SAT（Satisfiability）求解器来判断候选解是否为诊断。但该类方法存在对候选解空间的冗余解进行一致性检测的不足，因此，本文提出结合SAT的分组式诊断方法（Grouped Diagnosis，GD）实现电路元件的分组并剪枝这些冗余空间，以提高算法效率。该方法首先结合电路特征，利用单元传播规则获取故障输出，依据电路逻辑与故障输出将电路中元件进行分组。其次结合诊断问题和SAT求解过程的特征，给出非诊断定理和分组式诊断方法，并利用分组后的电路加速对集合枚举树无解空间的剪枝，进而提高算法求解效率。实验结果表明，针对获取所有极小子集诊断，在相同的诊断长度限制下，GD方法比目前最先进的结合集合枚举树的基于SAT的MBD方法求解效率更高。
2)MaxSAT（Maximal Satisfiability）技术也是用来解决MBD问题的高效方式之一，但其不需要额外的结构辅助，因此引出提高算法效率的另一种途径——对电路系统进行抽象，该方式可缩减问题规模。目前的抽象算法主要为基于分层抽象方法，该方法在抽象电路上得到顶层诊断（Top-Level Diagnosis，TLD），再对TLD进行迭代枚举替换操作，以得到所有的极小势诊断，但该方法的缺陷在于需要对拓展诊断逐一检查一致性，这个过程十分耗时。因此，本文给出一种结合MaxSAT的区域化抽象诊断方法（Zonal Diagnosis，ZD）。首先结合电路特征，提出新的抽象模型，将电路划分成不同的Zone，并利用MaxSAT求解器在由这些Zone构成的抽象电路上得到极小势抽象诊断。其次利用值传播特点提出了一种新的传播扩展方法，用于扩展极小势抽象诊断以有效地获得所有极小势诊断，从而避免检查一致性，提高求解效率。实验结果表明，针对获取所有极小势诊断，在相同的诊断数量限制下，ZD算法比目前最先进的基于分层抽象的算法求解时间更短，显著提高了算法效率。
3)健康态作为诊断算法求解质量的代表，该形式表示系统所有元件故障的可能性，在故障排除等问题中有十分重要的应用。健康态通过诊断列表及其分数计算而得，且不需要所有的诊断参与计算即可得到质量收敛的健康态，但不足之处在于该诊断列表中诊断均只解释一个观测，诊断的精确度较低，从而影响健康态质量。因此，本文设计一种结合多观测和差异度的提高健康态质量方法（Improve the Quality of Health State with Difference Degree，IHSD）来解决该问题，以获取更高质量的健康态。结合健康态计算时不需要所有诊断即可质量收敛的特征，该方法首先给出适应健康态计算的多观测MBD方法，利用多观测诊断方法对诊断进行整合，得到同时满足多观测的精确诊断。其次结合“差异度”概念对评分机制进行修改以对精确诊断进行评分，尽量提高精确诊断的分数以尽可能接近真实故障情况，从而提高健康态的质量。实验结果表明，设置相同的收敛参数，与目前最先进的计算健康态方法对比，IHSD算法显著提高了健康态的质量。
4)与单观测MBD方法相比，多观测MBD方法可对多个观测结果进行联合诊断以识别常见的故障位置，且该方法在程序故障定位等领域取得成功，针对基于一致性的组合电路多观测MBD问题，有学者给出两种完备方法，即诊断组合方法和碰集二元性方法。考虑到观测增量化的情况，诊断组合方法是合适的，但其在获取满足多观测的精确诊断过程中，无法完全避免非极小解情况的出现，仍需子集检测过程辅助，影响算法效率。因此，本文提出增量的多观测极小诊断方法（Incremental MBD with Multiple Observations，IMBDMO）。该方法首先给出极小子集精确诊断定理和诊断组合规则，确保精确诊断的子集极小性且避免子集检测过程，进而提高算法效率。其次实现观测增量化。实验结果表明，与目前最先进的诊断组合方法对比，IMBDMO算法显著提高了算法效率且在观测增量化情况下依然保证算法高效性。