基于SAT的故障树最小割集计算

摘要

故障树分析（FTA）是一种重要的可靠性分析方法，广泛应用于安全关键系统的可靠性分析与验证。求解故障树所有的最小割集（MCS），即寻找所有引发系统故障的最小的基本事件的组合，是FTA的关键问题。这一问题本身并不简单，其一直是学术和工业界讨论的热点。现有的这一问题的解决方法主要分为基于布尔代数以及基于二叉判定图（BDD）。对于一些特别复杂或者规模特别庞大的故障树，这些方法依然存在局限性。因此，我们的主要贡献在于提出了全新的基于可满足性问题（SAT）的故障树MCS求解算法。本文研究内容分为三个部分，具体内容如下所述。 首先，提出一个基本的基于SAT的故障树MCS求解算法——SATMCS。SATMCS采用类似Davis-Putnam-Loveland-Logeman（DPLL）的方式，不断迭代搜索故障树的MCS。通过启发式的策略，SATMCS可以避免对搜索空间的全部遍历。SATMCS的创新点如下所示：(a)Tseitin编码故障树，不仅使得编码效率得到提升，而且使得SATMCS可以得到故障树的结构特征，有助于启发式搜索策略的构建；(b)提出了基于割集覆盖的MCS提取算法，每次迭代通过求解一个MCS的近似来不断提取准确的MCS；(c)基于多优先度的独立启发式赋值策略，SATMCS可以利用故障树结构特征，趋向性地搜索MCS。 然后，通过对SATMCS的性能分析，明确SATMCS性能瓶颈在于最小割集的近似程度。为此，深度优化了SATMCS——SATMCS-Pro。SATMCS-Pro采用类似SATMCS基于搜索的MCS求解过程，根本性的变化在于MCS的提取算法。SATMCS-Pro的创新点如下所示：(a)提出了一种增量式的割集判定过程，提高了割集判定的效率；(b)提出了一种基于局部传播图的最小割集提取算法，精确高效地求解最小割集；(c)增量式地学习割集搜索过程产生的冲突子句以及最小割集对应的Block子句，加速搜索空间的剪枝过程；(d)我们的研究捕捉到了最小割集的分布规律，进而SATMCS-Pro采用Jump-chronological回溯策略提高了相邻两次迭代求解的信息共享程度，优化了搜索过程。 最后，实现了一个可以搭载SATMCS或SATMCS-Pro作为求解核心的故障树最小割集求解工具——NUAAFTA。从实验中，可以得出：SATMCS-Pro拥有优秀的求解故障树所有的最小割集的能力，其性能指标（内存和时间消耗）与商业软件具有可比性，甚至优于一些商业软件。

目录

第一个书签之前