[發明專利]變元的賦值順序及賦值優化算法、布爾可滿足性驗證算法

在審

• 申請號: 202011634036.7
• 申請日: 2020-12-31
• 公開（公告）號: CN112733350A
• 公開（公告）日: 2021-04-30
• 發明（設計）人: 劉美華;屈璋;張巖;黃國勇;金玉豐
• 申請（專利權）人: 國微集團（深圳）有限公司
• 主分類號: G06F30/20
• 分類號: G06F30/20;G06F11/36
• 代理公司: 深圳市康弘知識產權代理有限公司 44247
• 代理人: 尹彥

本發明公開了一種變元的賦值順序及賦值優化算法、布爾可滿足性驗證算法。其中分支啟發的變元的賦值順序優化算法，至少一個變元采用以下步驟確定賦值順序：將當前待賦值的變元作為當前變元；搜索與當前變元同時出現在同一子句中的關聯變元；累計所述關聯變元與當前變元同時出現在同一子句中的次數；選擇次數最少的關聯變元作為繼當前變元之后的待賦值的變元。本發明可以加快分支啟發算法的計算時間。

技術領域

本發明涉及等價性驗證工具中的布爾可滿足性驗證技術領域，尤其涉及分支啟發的變元的賦值順序優化算法、分支啟發的變元的賦值優化算法，以及采用了該賦值優化算法的布爾可滿足性驗證算法。

背景技術

布爾可滿足性驗證算法通常包含三個主要部分：分支啟發算法、演繹機制和BCP(即BCP傳播)、以及沖突分析和學習。

在布爾可滿足性驗證過程中，BCP傳播占用大部分的時間，一個好的分支啟發策略可以快速找到決策變元，減少沖突次數，加速BCP過程，因此，好的分支啟發策略對提高整個布爾可滿足性驗證工具的運行效率意義重大。現有使用最多的是VSIDS分支啟發策略，相比早期的分支啟發(出現次數最多優先、最短字句出現頻率最大優先、最短正子句優先、DLIS、DLCS)，VSIDS分支啟發策略可以更好的結合沖突分析過程，大大縮減BCP時間。以下為VSIDS算法的主要過程：

1、每一個變元的正、負文字都分配一個計數器s，并且初始值為0；

2、當學習子句加入到子句集時，該子句中所有的文字活性加1；

3、所有文字的活性分數定期除以一個大于1的常數；

4、每次分支決策時選擇計數器分值最高未賦值的文字進行賦值，在有多個相等計數器的情況下，隨機選擇一個文字進行賦值。

在搜索的初始階段，由于沖突次數較少，VSIDS的活性分數是不準確的，因此通過活性所選擇的分支決策具有一定的隨機性。簡單的說：如果把蘊含圖根據連接關系分解為社區結構，我們不確定所選擇的自由變元在社區內部還是聯接各個社區結構之間的橋接變量。只有隨著時間的推移，才能使VSIDS所選擇的變元具備一定的質量水平，此時所習得的學習子句質量也更高。

另一方面，初始變元的選擇，直接影響整個搜索過程，選擇不好的初始變元，在求解過程中雖然會產生大量沖突，但所習得的學習子句通常質量較低，會在子句庫刪減操作中刪除。對于大多數求解器，都是采用隨機賦值的方式選擇初始變元，這就會使求解過程的開始階段具備一定的局部性，即求解器此時主要關心初始變元所在的社區結構，也通常從最近的社區結構中挑選變元做分支決策，發生沖突并產生學習子句，然后才逐步擴散至橋接變量和其他社區結構。然而，橋接變量與其他社區結構的所產生的學習子句更能反應SAT問題實例的組織關系。所有造成了時間和空間的浪費。

發明內容

為了解決現有技術中隨機選擇變元進行賦值導致計算效率較低的技術問題，本發明提出一種變元的賦值順序及賦值優化算法、布爾可滿足性驗證算法。

其中分支啟發的變元的賦值順序優化算法，至少一個變元采用以下步驟確定賦值順序：

步驟1，將當前待賦值的變元作為當前變元；

步驟2，搜索與當前變元同時出現在同一子句中的關聯變元；

步驟3，累計所述關聯變元與當前變元同時出現在同一子句中的次數；

步驟4，選擇次數最少的關聯變元作為繼當前變元之后的待賦值的變元。

進一步，所述步驟4執行完畢后返回步驟1，直至同一字句的所有的變元的賦值順序確定。

進一步，所述當前待賦值的變元為分支啟發的第一個待賦值的變元或者為子句的第一個待賦值的變元。