[發明專利]一種布爾可滿足性問題求解方法及系統

在審

• 申請號: 202011545368.8
• 申請日: 2020-12-23
• 公開（公告）號: CN112487740A
• 公開（公告）日: 2021-03-12
• 發明（設計）人: 屈璋;劉美華;張巖;呂紅亮;黃國勇;畢舜陽
• 申請（專利權）人: 國微集團（深圳）有限公司
• 主分類號: G06F30/32
• 分類號: G06F30/32
• 代理公司: 深圳市康弘知識產權代理有限公司 44247
• 代理人: 尹彥

本發明公開了一種布爾可滿足性問題求解方法及系統，所述方法包括：采用多個并行求解器在設定的閾值條件內對CNF實例進行多線程并行求解，其中，每個并行求解器采用不同的初始變元；每個并行求解器在觸發閾值條件后停止求解，并記錄求解過程中各個變元的活性分數；選擇所述多個并行求解器得到的活性分數之和最高的變元作為主求解器的初始變元，對所述CNF實例進行求解。采用本發明的技術方案，可提高布爾可滿足性問題的求解速度。

技術領域

本發明涉及電子設計自動化（Electronic Design Automation，EDA）領域，尤其涉及一種布爾可滿足性問題求解方法及系統。

背景技術

可滿足性問題（SAT問題）是指給出一個以合取范式格式表達的命題邏輯公式，推理判斷是否存在一組或多組賦值使得這個合取范式表示的公式可滿足。在可滿足的情況下，算法會給出一組使得問題滿足的解。自2002年至2020年，大批高效的SAT求解器和先進的算法被不斷提出，其中算法主要分為兩種，即CDCL（conflict driven clause learning，沖突驅動子句學習）算法和SLS（stochastic local search，隨機局部搜索）算法。CDCL算法是基于DPLL算法的改進，對產生的沖突進行分析，引入沖突分析、子句學習策略和非時序性回溯策略，提高了算法求解效率。基于CDCL算法框架進行改進的SAT求解器如Chaff、MiniSat、Glucose等已經在SAT問題上取得了很大的效果，當前SAT的研究主要集中在分支啟發策略、單子句傳播、子句學習、重啟、預處理、非時序性回溯和數據結構的設計上。

Chaff的作者表明，在求解過程中BCP傳播占用了大量的時間，因此提出一種分支啟發策略給予持續出現在沖突中的變元較高的活性分數，這樣，在下一次決策時可以快速選擇變元，現有的變元分支啟發策略都是基于這種思路。

但是，在求解的初始階段仍然存在問題。一方面，在搜索的初始階段，由于沖突次數太少，分支啟發策略的選擇是不準確的，因此選擇分支變元具有一定的時間局限性。簡單的說，在初始階段，不能確定所選擇賦值的自由變元在命題邏輯結構中扮演者怎樣的邏輯角色，只有隨著時間的推移，才能通過分支啟發策略選擇具有一定質量水平的變元。另一方面，初始變元的選擇，直接影響整個搜索過程，選擇不好的初始變元，在求解過程中雖然會產生大量沖突，但所習得的學習子句通常質量較低，會在子句庫刪減操作中刪除。對于大多數求解器，都是采用隨機賦值的方式選擇初始變元，這就會使求解過程的開始階段具備一定的空間局限性。

在電子設計自動化領域，SAT求解器在搜索初始階段的時間局限性和空間局限性尤為明顯，原因在于：電子設計自動化領域往往通過先設計一些小的功能模塊，再用這些小的功能模塊來構筑復雜的電路，電路模塊內聯系緊密但各個電路模塊之間的聯系較少，聯接各個電路模塊之間的橋接變元具有劃分模塊的作用，即：通過分割橋接變元可以或多或少的獨立解決考慮電路模塊的內部關系。但此類問題轉化為SAT問題之后，可能會導致一些結構信息的缺失。而且，由于隨機選擇初始值，不能有效選擇在電路模塊中扮演橋接作用的變元。造成了時間和空間的浪費。在其他領域，如軟件開發等，也存在這種情況。

發明內容

本發明的目的是針對現有技術的SAT解算器隨機選取第一個分支變元導致解算初始階段存在時間局限性和空間局限性的技術問題，本發明提出一種布爾可滿足性問題求解方法及系統。

本發明實施例中，提供了一種布爾可滿足性問題求解方法，其包括：

采用多個并行求解器在設定的閾值條件內對CNF實例進行多線程并行求解，其中，每個并行求解器采用不同的初始變元；

每個并行求解器在觸發閾值條件后停止求解，并記錄求解過程中各個變元的活性分數；

選擇所述多個并行求解器得到的活性分數之和最高的變元作為主求解器的初始變元，對所述CNF實例進行求解。

本發明實施例中，所述設定的閾值條件包括求解過程中沖突的次數、求解器重啟的次數及求解器運行的時間。