一種求解命題公式骨干集的警示傳播算法*

王 帥，王曉峰，梁 田，李 志

(北方民族大學計算機科學與工程學院，寧夏 銀川 750021)

1 引言

骨干集一詞是在布爾可滿足性SAT(SATisfiability)問題相變研究中提出的[1 - 6]，一個可滿足命題公式的骨干集文字必將會出現在所有滿足指派中[7 - 10]，它對命題公式的可滿足性判定難度有重要影響[11 - 17]。骨干集越大，公式的判定難度越大。如果給定一個命題公式的骨干集，那么公式的判定將會變得容易。然而，一般情況下，求解命題公式的骨干集是困難的。目前，學術界主要使用以下幾種算法求解骨干集，最為基礎的是Marques-Silva等人[18]利用骨干文字位于所有的滿足指派中的性質，使用minisat求解器求出所有滿足指派，并使之相交得到骨干集。Janota等人[19]通過對文獻[18]方法的改進，提出一種更少迭代次數的骨干集求解算法，同時利用骨干文字反向賦值會使公式不滿足的性質，提出一種文字翻轉技術求解骨干集。Previti等人[20]利用抽象論證中理想語義和骨干集的聯系，設計一種新的主干網絡并利用帶有偏好的SAT求解器求解骨干集。Guo等人[21]以一次測試算法為基礎，運用啟發式思維設計出一種評分機制與過濾機制相結合的骨干集算法。de Haan等人[22]利用結構化實例中的局部骨干文字很大一部分都是全局骨干文字的特點，以局部計算的復雜度來判斷局部子句的骨干文字，進而求解骨干集。Zhu等人[23]利用集成電路中的錯誤空間和時間定位復雜化，設計了一個基于該技術的SAT求解方法，求解大規模公式中的骨干集。Ivrii等人[24]利用權重與數值等啟發式信息，在邏輯上假設骨干文字用以加快算法的搜索速度。Kilby等人[8,25]在求解后門集時也對骨干集進行了求解，對比2個集合發現后門集與骨干文字之間幾乎沒有交集，通過對后門集賦值化簡公式求解骨干集。上述方法都具有一定的局限性。

信息傳播算法是基于因子圖模型的一種信息迭代算法，已有的實驗結果和理論結果表明：信息傳播算法求解SAT問題效果較好，特別是對于因子圖為樹形結構的公式，算法能夠在多項式時間內給出問題的有效解。警示傳播WP(Warning Propagation)算法是信息傳播算法的一種最基本形態，其特點是基于信息傳播可以以高概率確定一個可滿足指派部分變元的取值，從而化簡公式。WP算法的基本思想是：在信息迭代過程中，根據當前子句的可滿足性對變元取值的依賴程度(概率)，“凍結”部分變元的取值。同時，在計算出子句中變元的取值傾向(概率表示)后，在子句與變元之間進行信息傳遞，使信息傳遞的值以較大概率決定變元的真值指派滿足給定公式。子句c與變元i之間這種傳遞取值傾向的概率為1時，表示子句c的可滿足性完全依賴于變元i的取值。對信息傳播算法的原理分析中發現，當算法收斂時，高概率凍結部分變元的賦值，可以對命題公式進行化簡。表明WP算法所“凍結”的變元，高概率是骨干集中的變元，因此本文設計一種求解命題公式骨干集的WP算法。

2 基礎知識

設子句集合F={a,b,…,}為一個具有m條子句的CNF公式，其中子句a中含有n個變量x1,…,xn。F可以用因子圖(Factor Graph)表示，因子圖可視為二分圖，圖中的節點可分為2類：一類是文字節點；另一類是子句節點。其中:

μa→i()表示子句a對文字xi的取值傾向;

V(i)表示包含文字xi的子句節點集合;

V(a)表示包含于子句a中的文字節點集合;

骨干文字：如果F={a1,…,am}是一個可滿足的公式，一個文字xi出現在所有的滿足指派中，那么文字xi就是骨干文字。

骨干集：文字的集合，指對于一個可滿足命題公式的每一個真值指派使得骨干集中的文字均為真。

2.1 警示傳播算法的基礎定義符號

(1)

(2)

(3)

其中，V-(j)表示變元xj負出現的子句集合。V+(j)表示變元xj正出現的子句集合。V(j)a表示變元xj出現的子句集合去除子句a。

顯然，

(4)

2.2 警示傳播算法的基本思想

μα→i(t+1)=

(5)

可化簡為式(6)所示：

(6)

其中，斷定函數如式(7)所示：

(7)

3 求解命題公式骨干集的警示傳播算法

(8)

(9)

(10)

所以式(10)對應于：

(11)

即ci=0時，通過Hi可以高概率地為文字xi賦值。當Hi≠0時，文字xi高概率地為骨干文字。

因此，本文設計骨干集求解算法，首先增加預處理過程，取消初始時刻對全部變量的隨機賦值，改為對特定子句和變量賦值化簡后再進行隨機賦值。其次利用WP算法的特性確定部分骨干文字，由于在化簡求解的過程中容易出現部分文字的Hi=0的情況，需要設計一個文字消除方法，消除特定Hi=0的文字，化簡整個公式，從而快速求解出骨干集。通過對WP算法過程的分析發現，子句會向文字傳遞趨向值，不同取值傾向子句個數相同，該文字就是需要消除的特定文字即非骨干文字。可知在求解命題公式骨干集的問題時，Hi不為0的文字是骨干文字，對文字進行賦值并對公式進行化簡，可以得到新的公式和骨干文字，反復迭代直到不收斂，即可得到一組通過Hi獲得的骨干文字。因此，去除式(11)中對xi的隨機賦值，確定所有的xi賦值，并對圖進行化簡進行下一輪計算。本文算法設計如算法3所示。

輸入:CNF公式F的因子圖，最大迭代步數tmax。

1. 對因子圖的單位子句賦值；

2. 將剩下的每條邊進行隨機賦值；

3.fort=1 totmax

4. 調用算法2更新(μa→i(t-1)→μa→i(t))；

6.endfor

7. 輸出結果。

輸入:警示信息μb→j:b∈V(j)a,xj∈V(a)xi。

輸出:新的μa→i。

1. 當V(a)xi=?，輸出μa→i=1；

2.forj∈V(a)xi

3.ifV(j)a=?

4.Hj→a=0；

5.else

6.hj→a=(∑b∈V+(j)aμb→j)-(∑b∈V-(j)aμb→j)；

7.endif

8.endfor

算法3求解命題公式骨干集的警示傳播算法

輸入:命題公式，最大迭代次數iter。

輸出:狀態標識，骨干集。

1.for迭代次數t=1 toiter

3.if本文WP算法不收斂

4. 退出；

5.else

6. 計算所有Hi和沖突標識ci;

7.WhileHi≠0do

8. 當Hi>0時，令xi=1;

9.當Hi<0時，令xi=0;

10.消除Hi=0中趨向值個數相等的文字，進行圖化簡;

11.endwhile

12.endif

13.endfor

14.輸出賦值結果，即骨干集。

4 實驗與結果分析

實驗主要從3個方面進行對比分析：(1)使用WP算法在不同類型的實例集上進行收斂性測試，分析算法的可行性。(2)在相同的實例集上與一次迭代算法Iterative SAT Testing(iter)[18]、核心文字翻轉算法Core-based Algorithm(core)[19]和局部骨干算法Iterative Local Backbones(lb)[22]等經典算法對比分析算法的求解時間。(3)在相同的實例集上對比近幾年常用的核心翻轉算法[19]和評分過濾算法[21]，分析算法的收斂性和準確度。

4.1 算法的可行性

為了測試算法的可行性，使用不同類型的實例集進行收斂性測試，只有收斂的實例才可通過WP算法進行骨干集的求解。選取了實際生產中常見的樹形因子圖、正則3.4Sat和隨機Sat這幾種結構不同的測試集。使用算法1對不同的實例進行收斂性測試，結果如圖1所示。

Figure 1 Convergence of different instances圖1 不同實例的收斂性

通過圖1可知，本文WP算法在樹形因子圖的實例集上必定收斂，在隨機Sat和正則3.4Sat上當子句/變元比值小于3.5時也必定收斂、大于3.5的部分也具有較好的收斂性。因此，實驗結果表明，本文WP算法在絕大部分實際生產問題中都具有較好的收斂效果。證明了本文WP算法對骨干集求解的可行性。

4.2 與經典算法的時間對比

分析了算法的可行性后，算法的運行時間往往也是求解命題公式骨干集的關鍵。本文構建了n=200,400,600的樹形因子圖和隨機Sat因子圖進行對比實驗。用本文WP算法和其它經典的骨干集算法對相同類型的因子圖的多個實例進行求解，對比不同算法求解時間，結果如圖2～圖4所示。

Figure 2 Solution time of each algorithm with n=200圖2 n=200時各算法的求解時間

Figure 3 Solution time of each algorithm with n=400圖3 n=400時各算法的求解時間

Figure 4 Solution time of each algorithm with n=600圖4 n=600時各算法的求解時間

Figure 5 Time comparison on fla problem of three algorithms圖5 3種算法在fla問題上的時間對比

通過圖2～圖4可知，隨著變元數目的不斷增加，本文WP算法明顯優于經典的骨干集求解算法。在本實驗中，發現當變元數目在400～600時，本文WP算法和lb算法的求解時間有優勢，而且隨著變元數目增多，其時間優勢逐漸增大。而且本文WP算法相較于lb這類近似算法，在求解隨機Sat問題上具有一定的時間優勢，但在結構性實例上優勢不明顯。同時實驗發現隨著變元的增多，本文WP算法的求解時間呈線性增長，相對于經典算法的求解時間的增長幾乎可以忽略不計。即可理解為本文WP算法在求解變元數目較多的實例上相對于經典算法具有非常明顯的優勢。

4.3 與目前常用算法的時間對比

在求解骨干集的算法中，大部分都是進行局部求解，然后根據局部解推測出全局解。目前最為常用的骨干集算法是Janota等人[19]提出的文字翻轉算法和Guo等人[21]設計的啟發式評分過濾算法。在相同實例下對比2種算法與本文WP算法的求解效果，結果如圖5所示。

從圖5中可以發現，本文WP算法在求解命題公式骨干集時，隨著問題復雜性的增大，求解時間優于另外2種算法。

5 結束語

本文通過對WP算法的修改，設計一種求解命題公式骨干集的警示傳播算法，該算法在構建的特殊命題公式上求解的速度都較快，在SAT-encoded “Flat” Graph Colouring Problems(fla)基準集上求解速度比構建的特殊命題公式慢。但是，與文字翻轉算法和啟發式評分過濾算法相比還是有所提高的。

在后期的工作中，考慮通過使用弱后門集與骨干集沒有交集的理論，對WP算法進行改進，使其能求解出更多的骨干文字。