[發明專利]一種基于跳躍回溯的故障樹最小割集求解方法

在審

• 申請號: 201810309389.6
• 申請日: 2018-04-09
• 公開（公告）號: CN108388764A
• 公開（公告）日: 2018-08-10
• 發明（設計）人: 魏歐;羅煒麟;李思潔;王立松
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F19/00
• 分類號: G06F19/00
• 代理公司: 南京鐘山專利代理有限公司 32252
• 代理人: 戴朝榮

本發明提供了一種基于跳躍回溯的故障樹最小割集求解方法。所述基于跳躍回溯的故障樹最小割集求解方法包括如下步驟：一、根據最新求解得到的最小割集，計算決策等級；二、SATMCS回溯到步驟一得到決策等級，進行布爾約束傳播過程；三、SATMCS進入下一個決策等級，繼續搜索割集。本發明的有益效果是：所述基于跳躍回溯的故障樹最小割集求解方法可以有效利用故障樹的最小割集求解空間分布聚合的特性，有效提升SATMCS求解故障樹最小割集的效率。

技術領域

本發明屬于故障樹分析技術領域，具體地涉及一種基于跳躍回溯的故障樹最小割集求解方法。

背景技術

可滿足性問題(Boolean Satisfiability Problem，SAT)是判斷布爾公式的滿足性問題。這一問題是計算機理論與應用的核心問題。SAT是NP-complete(NPC)問題，是眾多問題求解效率的性能瓶頸，包括約束滿足(ConstraintSatisfaction)、擴展推理(ExtendInference)、定理證明(TheoremProving)等領域。

接下來介紹SAT的相關概念。對于包含m個布爾變量的集合文字(Literal)是一個布爾變量或者是v_i的非(Negation)分別稱為v_i的正文字(Positive Literal)和負文字(Negative Literal)，v_i和互補(Opposite)；積(Product)是文字的合取，積可以表示為文字的集合；定義在上的賦值(Assignment)是一個映射賦值可以由一個積π表示；子句(Clause)是文字的析取；對于積π，由得到的子句稱為Block子句(BlockClause)；合取范式(Conjunctive NormalForm，CNF)是子句的合取，可以寫成集合的形式；析取范式(Disjunctive Normal Form，DNF)是積的析取。

Davis-Putnam-Loveland-Logeman(DPLL)是一類主流的求解SAT的確定性算法框架，結構如圖1所示。整個框架分為四個模塊：DECIDE、BCP、ANALYZECONFLICT和BACKTRACK。算法的輸入是CNF范式表示的布爾公式f。輸出是f的可滿足性情況。若f存在可滿足解，那么輸出一個可滿足解，否則輸出不可滿足。DPLL是一個分支搜索算法，其搜索過程可以看成對二叉樹的深度優先遍歷。其算法的總體思想是通過不斷迭代為變量賦值；利用布爾約束不斷減少搜索空間，盡可能趨向性地搜索滿足輸入的賦值；直到找到一個可以使得輸入滿足的賦值或者判定輸入是不可滿足為止。

初始狀態下所有的變量均未賦值，稱為自由變量(Free Variable)。在每次迭代過程中，DECIDE采用啟發式的賦值策略選擇f中的自由變量x，并賦值。通過啟發式的賦值策略，DPLL可以盡可能趨向性地搜索可滿足解。這一過程中，如果不存在自由變量，表示DPLL得到一個可滿足的賦值，結束算法；否則，開始一個全新的搜索分支。搜索的深度由決策等級(Decision Level)dlevel表示。dlevel從0開始，每次DECIDE前均加1，表示即將進入相比于上一個決策等級更深一層的搜索分支。之后，算法得到一個部分賦值π，進入布爾約束傳播(Boolean Constraint Propagation，BCP)過程。BCP基于單位子句規則(Unit ClauseRule)通過f所提供的布爾約束關系和π推導出新的自由變量的賦值。單位子句c_i指的是這樣的子句：π使得c_i中只有一個自由變量且c_i未被滿足。單位子句規則是一種推導方法，它將從單位子句中推導出新的變量賦值。例如對于子句若當前部分賦值為此時c_i是單位子句。根據單位子句規則，BCP更新DECIDE和BCP中被賦值的變量x均對應當前的決策等級dlevel，記為x@dlevel(x被賦值為TRUE)或(x被賦值為FALSE)。