范全潤,段振華,2

(1.西安電子科技大學(xué)計(jì)算理論與技術(shù)研究所,陜西西安 710071; 2.西安電子科技大學(xué)綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國家重點(diǎn)實(shí)驗(yàn)室,陜西西安 710071)

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

范全潤1,段振華1,2

(1.西安電子科技大學(xué)計(jì)算理論與技術(shù)研究所,陜西西安 710071; 2.西安電子科技大學(xué)綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國家重點(diǎn)實(shí)驗(yàn)室,陜西西安 710071)

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

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

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

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

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

因?yàn)橄ス沧兞啃枰鄳?yīng)的時(shí)間代價(jià),因此,一個(gè)好的聚類算法應(yīng)該盡量減少簇間公共變量的個(gè)數(shù).

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

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

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

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

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

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

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

圖1　一個(gè)布爾公式的子句之間的聯(lián)系圖

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

為避免這一情況,文中提出在聚類的第1階段采用基于連接的聚類方法來避免聚類的局部性.本節(jié)提出的算法以文獻(xiàn)[6]為基礎(chǔ),并根據(jù)布爾子句的特點(diǎn)進(jìn)行了相應(yīng)調(diào)整.

1.1相關(guān)概念

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

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

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

1.2連接的計(jì)算方法

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

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

1.3基于連接的聚類

如果每次找連接最多的兩個(gè)簇進(jìn)行合并,則算法會(huì)優(yōu)先合并大的簇,因?yàn)榇蟮拇刂g的連接數(shù)更多.為避免這一情形,算法中用合并評(píng)價(jià)函數(shù)g(Ci,Cj)的值來決定要合并哪兩個(gè)簇.g(Ci,Cj)定義為

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

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

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

為快速找到當(dāng)前應(yīng)該合并的兩個(gè)簇,算法使用一個(gè)全局隊(duì)列Q,對(duì)于一個(gè)簇Cj,max(q[j])代表和簇Cj合并的最佳簇,g(j,max(q[j]))則為這兩個(gè)簇合并的評(píng)價(jià)函數(shù)的值,全局隊(duì)列Q中的簇按合并質(zhì)量函數(shù)的值降序排列.

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

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

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

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

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

3　實(shí)驗(yàn)驗(yàn)證

針對(duì)SAT數(shù)據(jù)庫[7]和2013年SAT競賽中應(yīng)用部分的基準(zhǔn)用例[8],用文中提出的兩階段聚類算法進(jìn)行了實(shí)驗(yàn),得出的實(shí)驗(yàn)結(jié)果如表1所示.在表1中省去了文件的.cnf的擴(kuò)展名.

在算法的第1階段,實(shí)驗(yàn)中將最終生成的簇的數(shù)目定義為原始簇?cái)?shù)目的一半.在第2階段,根據(jù)相似度來確定是否終止聚類算法的執(zhí)行.兩個(gè)階段中使用的相似度閾值相同.表1中第5列和第6列分別表示單獨(dú)用相似度法和兩階段取類方法得到的簇之間的共同變量的數(shù)目.通過實(shí)驗(yàn)發(fā)現(xiàn),兩階段法比單獨(dú)利用相似度法能得到更好的結(jié)果.

表1　CNF文件聚類結(jié)果

4　結(jié)束語

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

但是,這種兩階段的聚類算法和使用兩兩相似度的聚類算法相比,需要耗費(fèi)更多的時(shí)間用于連接的計(jì)算.下一步將考慮優(yōu)化聚類過程中連接的計(jì)算方法.

[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].軟件學(xué)報(bào),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模體發(fā)現(xiàn)聚類求精算法[J].西安電子科技大學(xué)學(xué)報(bào),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]劉逸,寇衛(wèi)東,慕彩紅.結(jié)合多閾值法的模糊聚類用于SAR圖像變化檢測[J].西安電子科技大學(xué)學(xué)報(bào),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

時(shí)間:2015-07-27

國家自然科學(xué)基金資助項(xiàng)目(61133001,61322202,61420106004)

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

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