一種布爾子句的兩階段聚類方法

范全潤,段振華,2

(1.西安電子科技大學計算理論與技術研究所,陜西西安 710071; 2.西安電子科技大學綜合業務網理論及關鍵技術國家重點實驗室,陜西西安 710071)

一種布爾子句的兩階段聚類方法

范全潤1,段振華1,2

(1.西安電子科技大學計算理論與技術研究所,陜西西安 710071; 2.西安電子科技大學綜合業務網理論及關鍵技術國家重點實驗室,陜西西安 710071)

針對布爾子句的聚類問題,根據合取范式布爾子句的特點,提出了一種兩階段的子句聚類方法.初始時每個子句被看作1個簇,第1階段的聚類采用基于連接的方法,根據兩個子句或者子句組之間的共同鄰居的個數來決定是否要合并它們;第2階段根據子句或者子句組之間的相似度來進行聚類.該方法的第1階段采用全局的觀點來實現子句的聚類,在一定程度上避免了聚類的局部性最優性,第2階段利用相似度來決定是否合并兩個簇,因而無需指定聚類結果中簇的個數.實驗結果表明,該聚類方法得到的結果中公共變量的個數較少,聚類結果更好.

布爾合取范式;子句;聚類;連接

布爾可滿足性問題(Propositional Satisfiability,SAT)在計算機科學領域具有重要的理論意義和實用價值,它是第1個被證明的非確定多項式完全(Non-deterministic Polynomial-Complete,NPC)問題[1].給定一個布爾命題公式,SAT判定就是要找到一組變量的賦值,使得該命題的公式為真,即該公式可滿足;或者證明該命題公式不可能為真,即該公式不可滿足.

大部分SAT判定工具采用的算法都是基于系統搜索,在最壞的情況下,系統搜索需要窮舉所有變量的取值組合來判定公式的可滿足性,因此,算法的時間復雜度為O(2n),其中,n為公式中變量的個數.雖然近年來SAT的判定研究取得了很大的進展,但在實踐中,還有很多SAT判定問題目前無法解決.

目前絕大部分SAT判定工具都要求輸入是合取范式(Conjunctive Normal Form,CNF)形式,而文中的研究正是針對CNF公式的可滿足性判定問題.如果利用聚類技術將CNF公式聚類成多個簇,然后消去簇間的公共變量,就可將原公式的聚類問題轉化為幾個子問題來求解.消去公共變量后,一個布爾公式F中的子句可劃分為m個子句組C1,C2,…,Cm,每個子句組中包含的變量集合分別為S1,S2,…,Sm,這些變量集兩兩不相交,即對任意的1≤i≤m,1≤j≤m,i≠j,有Si∩Sj=?,則布爾公式F是可滿足的,當且僅當它的劃分子句組C1,C2,…,Cm都是可滿足的;布爾公式F是不可滿足的,當且僅當它的某個劃分子句組Ci(1≤i≤m)是不可滿足的.

因為消去公共變量需要相應的時間代價,因此,一個好的聚類算法應該盡量減少簇間公共變量的個數.

如果采用層次凝集的聚類方法,首先將每個布爾子句作為1個簇,然后根據子句之間的相似度來將數據對象進行合并,直至達到某一終止條件.由于合并時只考慮兩個簇之間的相似度,因此,這種聚類方法可能不是全局最優的.

基于連接的聚類方法將相似度超過設定閾值的兩個子句(或子句組)定義為鄰居,兩個子句之間的連接定義為這兩個子句之間的共同鄰居的數目.根據連接來進行聚類,考慮了子句和它的鄰居之間的聯系,因而更有可能產生好的聚類結果,但是這種方法需要指定最終生成的簇的數目.

筆者針對CNF的特點,給出了一種布爾子句相似度的定義,提出了一種兩階段的聚類方法.公式中的每個子句被當作1個簇,聚類的第1階段采用基于連接的聚類方法,在一定程度上避免基于相似度的方法存在的局部最優的缺點.第2階段采用基于兩兩相似度的方法,當所有簇之間的相似度都小于設定的閾值時就終止聚類,從而無需指定最終生成的簇的數目.

1　基于連接的布爾子句聚類方法

沒有任何一種聚類算法或者技術可以普遍適用于各種類型數據集的聚類,這其中的原因之一就是因為很難給出簇的精確定義[2].根據數據在聚類中的集聚規則以及應用這些規則的方法,可將聚類算法大致劃分為層次化的聚類算法(基于聯接的聚類算法)、基于劃分的聚類算法、基于密度和網格的聚類算法和其他聚類算法[3-5].

文中所用的聚類方法是一種凝聚的層次聚類方法,即首先將每個布爾子句看作1個簇,然后通過選擇合適的兩個簇,將它們合并為1個簇,重復這一過程直到產生最終的聚類結果.從上面的分析可看出,要從一個CNF公式產生好的子句組劃分,應該盡量減少不同的子句組之間的共同變量個數,也就是應該將包含相同變量多的子句歸到同一個子句組,將包含共同變量少的子句歸到不同的子句組.這樣,才能降低消去這些變量所需的代價.

但是,如果僅是根據數據對象間的相似度,可能不會產生較好的聚類結果.例如,假定在圖1中,每個頂點代表1個子句,邊代表兩個相應的頂點之間存在的共同變量.從圖1可以看出,如果將子句聚類為兩個簇,一個簇中包含子句{2,3,4,5,6},另一個簇中包含子句{7,8,9,10,1},則這種聚類結果較為理想.

圖1　一個布爾公式的子句之間的聯系圖

但是,如果采用的是基于數據點之間的兩兩相似度的方法,假定子句1和子句2之間的相似度超過了設定的閾值,則這樣的聚類方法就有可能先將子句1和子句2聚類到同一個簇中,導致聚類不能產生理想的結果.

為避免這一情況,文中提出在聚類的第1階段采用基于連接的聚類方法來避免聚類的局部性.本節提出的算法以文獻[6]為基礎,并根據布爾子句的特點進行了相應調整.

1.1相關概念

(1)鄰居.如果兩個布爾子句或者簇之間的相似度大于設定的閾值,則稱它們是鄰居.用sim(Ci,Cj)來表示兩個子句Ci和Cj之間的相似度函數值.

(2)簇之間的相似度.針對CNF表示的布爾公式的特點,兩個子句或簇C1和C2之間的相似度定義為

(3)連接.用lin k(Ci,Cj)表示兩個子句或者簇Ci和Cj之間的連接數,即這兩個數據點之間的共同鄰居的數目.由連接的定義可知,如果lin k(Ci,Cj)的值越大,它們的共同鄰居就越多,這兩個簇就更應該合并.

1.2連接的計算方法

對于每個布爾子句或者布爾子句組成的簇,首先根據相似度計算出它的鄰居,對每個簇和它的鄰居組成的對,該簇貢獻了一個連接.對每個簇重復這一過程,就可計算出連接的數目.算法1給出了計算連接的方法,算法中C表示子句或者初始的簇的集合,lin k(i,j)表示兩個簇i和j之間的連接數目.

算法1 computeLinks(C) //計算子句(簇)之間的連接

1.3基于連接的聚類

如果每次找連接最多的兩個簇進行合并,則算法會優先合并大的簇,因為大的簇之間的連接數更多.為避免這一情形,算法中用合并評價函數g(Ci,Cj)的值來決定要合并哪兩個簇.g(Ci,Cj)定義為

其中,ni和nj分別表示簇Ci和Cj中的子句的個數,是簇Ci和Cj間期望的連接數目[6].

基于連接的聚類算法如算法2所示.它的輸入是初始的聚類C(每個布爾子句被當作一個簇),以及聚類結果中簇的數目k.對每一個簇Ci,設一個隊列q[i],此隊列中包括有和簇Ci的連接不為0的所有的簇的編號以及相應的合并評價函數的值.如果簇Ci的隊列中存在項(j,10),則表明有一個簇Cj和Ci之間存在連接,且g(Ci,Cj)的值為10.隊列中的元素按照g(Ci,Cj)值遞減排列,因此,根據隊首元素就可確定應最先和簇Ci合并的簇.

算法2 cluster(C,k) //聚類算法

為快速找到當前應該合并的兩個簇,算法使用一個全局隊列Q,對于一個簇Cj,max(q[j])代表和簇Cj合并的最佳簇,g(j,max(q[j]))則為這兩個簇合并的評價函數的值,全局隊列Q中的簇按合并質量函數的值降序排列.

算法2中while循環的終止條件是全局隊列Q中只剩下k個簇,或者在循環過程中出現所有的簇之間的交叉連接數都為0.在while循環中,使用extract Max()函數來找到合并質量函數值最大簇u,而隊列q[u]則被用來決定和最應優先合并的簇v.在第10行中,簇u和簇v合并產生一個新的簇w,這一合并需要對隊列進行相應的處理:隊列中的簇u或簇v需要用簇w來代替,并更新相應的link的值;需要為簇w創建相應的隊列,并對相應的隊列進行更新.

2　基于相似度的布爾子句聚類

基于連接的聚類算法存在一個缺點,它需要指定聚類的最終結果中所包含的簇的數目.但是,對于布爾子句的聚類,筆者希望用一種自然的方式來確定最終生成的簇的數目.為達到這一目的,在聚類的第2階段,文中采用基于簇間的兩兩相似度的方法來決定是否合并兩個簇.當所有簇之間的相似度都小于設定的閾值時,就得到最終的聚類結果,從而無需指定最終生成的簇的數目.

基于兩兩相似度的聚類方法如算法3所示.算法中的3個輸入C、min?cluster和threshold分別表示第1個聚類階段得到的初始聚類、期望的簇個數的最小值以及相似度閾值.為避免將所有子句聚類到一個簇,算法中用min?cluster來控制聚類結果中簇的個數,如果本次聚類后結果中簇的個數小于min?cluster,則返回本次聚類之前的結果,即Cmin;否則,重復聚類過程,以避免出現當相似度閾值設置過小時,會將所有子句聚類成一個簇的情況.相似度閾值決定兩個簇之間的相似度大到什么程度時對兩個簇進行合并.如果相似度閾值設置得較大,則最終產生的簇的個數就會比較多,相應的割變量總個數也會增多;反之,如果相似度閾值設置得較小,則簇的個數和割變量數也會相應減少.

算法3 CNF?Clustering(C,min?cluster,threshold) //基于相似度的聚類

3　實驗驗證

針對SAT數據庫[7]和2013年SAT競賽中應用部分的基準用例[8],用文中提出的兩階段聚類算法進行了實驗,得出的實驗結果如表1所示.在表1中省去了文件的.cnf的擴展名.

在算法的第1階段,實驗中將最終生成的簇的數目定義為原始簇數目的一半.在第2階段,根據相似度來確定是否終止聚類算法的執行.兩個階段中使用的相似度閾值相同.表1中第5列和第6列分別表示單獨用相似度法和兩階段取類方法得到的簇之間的共同變量的數目.通過實驗發現,兩階段法比單獨利用相似度法能得到更好的結果.

表1　CNF文件聚類結果

4　結束語

針對CNF布爾子句的特點,提出了一種兩階段的聚類算法.第1階段使用基于連接的聚類方法,根據兩個子句簇之間的共同鄰居的數目來確定優先合并的簇,避免了基于兩兩相似度的算法可能產生的局部最優問題.第2階段利用相似度來進行聚類,從而無需在算法中指定聚類最終產生的簇的數目.這樣,既可以在一定程度上避免聚類的“局部性”,又無需指定最終生成的簇的數目,使最終生成的簇的數目更自然.

但是,這種兩階段的聚類算法和使用兩兩相似度的聚類算法相比,需要耗費更多的時間用于連接的計算.下一步將考慮優化聚類過程中連接的計算方法.

[1]COOK S A.The Complexity of Theorem Proving Procedures[C]//Proceedings of the Third Annual ACM Symposium on Theory of Computing.New York:ACM,1971:151-158.

[2]ESTIVILL-CASTRO V.Why so Many Clustering Algorithms[J].ACM SIGKDD Explorations Newsletter,2002,4 (1):65-75.

[3]孫吉貴,劉杰,趙連宇.聚類算法研究[J].軟件學報,2008,19(1):48-61. SUN Jigui,LIU Jie,ZHAO Lianyu.Clustering Algorithms Research[J].Journal of Software,2008,19(1):48-61.

[4]張懿璞.一種新的DNA模體發現聚類求精算法[J].西安電子科技大學學報,2014,41(6):95-99. ZHANG Yipu.Novel Cluster Refinement Algorithm for DNA Motif Discovery[J].Journal of Xidian University,2014,41(6):95-99.

[5]劉逸,寇衛東,慕彩紅.結合多閾值法的模糊聚類用于SAR圖像變化檢測[J].西安電子科技大學學報,2013,40(6): 13-18. LIU Yi,KOU Weidong,MU Caihong.Change Detection for SAR Images Based on Fuzzy Clustering Using Multilevel Thresholding[J].Journal of Xidian University,2013,40(6):13-18.

[6]GUHA S,RASTOGI R,SHIM K.ROCK:a Robust Clustering Algorithm for Categorical Attributes[J].Information Systems,2000,25(5):345-366.

[7]HOOS H H,STüTZLE T.SATLIB:an Online Resource for Research on SAT[C]//Proceedings of the SAT.Amsterdam: IOS Press,2000:283-292.

[8]BALLNT A,BELOV A,HEULE M J H,et al.SAT Competition 2013 Solver and Benchmark Descriptions[C]//Proceedings of the SAT Competition 2013.Helsinki:University of Helsinki,2013:93-124.

(編輯:齊淑娟)

Two phase clustering method for CNF clauses

FAN Quanrun1,DUAN Zhenhua1,2
(1.Research Inst.of Computing Theory&Technology,Xidian Univ.,Xi’an 710071,China; 2.State Key Lab.of Integrated Service Networks,Xidian Univ.,Xi’an 710071,China)

Aimed at the Boolean clauses clustering,a two phases clustering method for CNF clauses is proposed.At the beginning,each clause is treated as a cluster.In the first phase,by a link based clustering method,the common neighbors between two clusters is used to determine how to merge the clusters.In the second phase,a similarity based clustering method is used.The first phase uses a global view to cluster the clauses,so the global optimum can be achieved in some sense.The second phase uses similarity to merge clusters,so the setting of the number of the final clusters in the algorithm is unnecessary.Experimental results show that the proposed method can lead to better clustering results with fewer common variables. Key Words: Boolean conjunctive normal form;clauses;clustering;links

TP311

A

1001-2400(2016)03-0055-06

10.3969/j.issn.1001-2400.2016.03.010

2015-01-20

時間:2015-07-27

國家自然科學基金資助項目(61133001,61322202,61420106004)

范全潤(1973-),男,副教授,西安電子科技大學博士研究生,E-mail:fqr?xd@126.com.

http://www.cnki.net/kcms/detail/61.1076.TN.20150727.1952.010.html