[發明專利]基于擴展規則的布爾可滿足性問題的求解方法

在審

• 申請號: 201910747374.2
• 申請日: 2019-08-14
• 公開（公告）號: CN110689128A
• 公開（公告）日: 2020-01-14
• 發明（設計）人: 王金艷;胡春;李先賢
• 申請（專利權）人: 廣西師范大學
• 主分類號: G06N5/04
• 分類號: G06N5/04
• 代理公司: 45107 桂林市持衡專利商標事務所有限公司
• 代理人: 陳躍琳

本發明公開一種基于擴展規則的布爾可滿足性問題的求解方法，首先，設計了適用于擴展規則的CCA_ER啟發式以及PAWS_ER規劃，并且發明了變量的Subscoer_er屬性和CScore_er屬性。其中CCA_ER啟發式是給超過一定閾值但格局沒有發生改變的變量一定的翻轉機會，而PAWS_ER規劃主要是用于更新子句權重。并且對于處于相變區間的實例，我們采用變量的CScore_er屬性；對于沒有處于相變區間的實例，我們采用變量的Subscoer_er屬性。接著，在初始化時利用IMOM思想得到初始極大項，使得初始解更加靠近實際解空間，減少了翻轉次數。最后在搜索過程中先判斷子空間的可滿足性，如果可滿足，則找到一個解，否則繼續判斷整個空間的可滿足性。

技術領域

本發明涉及布爾可滿足性問題求解技術領域，具體涉及一種基于擴展規則的布爾可滿足性問題的求解方法。

背景技術

布爾可滿足性問題(Boolean Satisfiability Problem，簡稱SAT問題)是一個著名的判定問題，不僅在數理邏輯和計算理論等方面有著舉足輕重的研究地位，而且在實際生產領域具有很高的應用價值。SAT問題是邏輯學的一個基本問題，也是當今計算機科學和人工智能研究的核心問題。工程技術、軍事、工商管理、交通運輸及自然科學研究中的許多重要問題，如程控電話的自動交換、大型數據庫的維護、大規模集成電路的自動布線、軟件自動開發、機器人動作規劃等，都可轉化成SAT問題。因此致力于尋找求解SAT問題的快速而有效的算法，不僅在理論研究上而且在許多應用領域都具有極其重要的意義。

近年來，對于SAT問題的求解，楊洋等人將擴展規則與局部搜索相結合，設計并實現了一種新的基于局部搜索的擴展規則推理方法(ERACC算法)。ERACC算法在搜索由極大項組成的搜索空間時，首先初始化一個極大項，然后利用局部搜索技術對極大項空間進行搜索，并且采用新的格局檢測避免陷入局部最優，算法每次選擇極大項當中的一個變量進行翻轉，直至找到一個不能擴展的極大項。雖然，ERACC算法在與現有的基于擴展規則的算法相比，具有較高的求解效率。但是，ERACC算法在避免陷入局部最優時，采用的是CC_ER啟發策略，該CC_ER啟發思想的原則是如果一個變量自從上次翻轉以來，格局沒有改變，則禁止翻轉，即使其翻轉能夠帶來很多益處，這在一定程度上影響了ERACC算法的求解效率。

發明內容

本發明提供一種基于擴展規則的布爾可滿足性問題的求解方法，其能夠進一步提升SAT問題求解的求解效率。

為解決上述問題，本發明是通過以下技術方案實現的：

基于擴展規則的布爾可滿足性問題的求解方法，具體包括步驟如下：

步驟1、設定最大主迭代次數maxStep和最大次迭代次數subMaxStep；令CNF公式集中所有子句的初始權值均為1，CNF公式集中所有變量的初始格局改變狀態為1，迭代次數i為0；

步驟2、根據輸入的CNF公式集，得到輸入變量集M及其變量個數MCount，以及輸入子句集C及其子句個數CCount；

步驟3、首先遍歷CNF公式集得到其中最長子句集S；然后遍歷最長子句集S，并記錄每個文字出現的次數；最后將所有文字按出現次數進行排序，并將出現次數較多前K位的文字的否定形成限定子句u；其中K為設定值；

步驟4、將限定子句u中的文字轉成變量形式后，放入到限定變量集W中，并將輸入變量集M與限定變量集W的差集中的變量放入到隨機變量集Y中；

步驟5、對于隨機變量集Y中的每個變量，隨機選擇每個變量的文字來與限定子句u中文字進行合并，形成初始極大項；