基于聚類的SAT實(shí)例結(jié)構(gòu)分析.pdf

1、隨著信息技術(shù)地不斷發(fā)展和移動(dòng)互聯(lián)網(wǎng)時(shí)代的到來，信息量出現(xiàn)了爆炸式的增長(zhǎng)，如何有效地利用這些數(shù)據(jù)成為一個(gè)非常熱門的研究方向。數(shù)據(jù)挖掘就是從大量數(shù)據(jù)中分析并找出隱含、有價(jià)值的信息的過程。SAT問題（satisfiability problem，簡(jiǎn)稱SAT），即布爾可滿足性問題，它是一個(gè)邏輯命題，即給定一個(gè)命題范式，判斷是否存在一組變量的賦值使得該范式為真。
　　近年來，對(duì)于SAT問題的研究主要是以局部搜索算法為基礎(chǔ)，在算法中加入新的策

2、略。雖然可以在一定程度上改善算法性能，但是對(duì)于大型SAT算例，由于子句之間聯(lián)系的復(fù)雜性，使得SAT實(shí)例存在潛在的結(jié)構(gòu)性特征，局部搜索算法在求解過程中容易出現(xiàn)相同變?cè)l繁翻轉(zhuǎn)、真子句數(shù)量無法改善等問題。所以，可以從SAT實(shí)例的角度對(duì)SAT問題進(jìn)行研究，通過數(shù)據(jù)挖掘技術(shù)分析SAT實(shí)例中子句與子句之間，變?cè)c子句之間潛在的結(jié)構(gòu)特征。首先，將SAT實(shí)例表示成圖結(jié)構(gòu)模型，頂點(diǎn)表示SAT實(shí)例中的子句，邊表示子句與子句之間聯(lián)系緊密程度；然后采用SAT

3、實(shí)例團(tuán)體結(jié)構(gòu)挖掘算法對(duì)SAT實(shí)例的圖結(jié)構(gòu)模型進(jìn)行挖掘，找出圖結(jié)構(gòu)模型中的團(tuán)體結(jié)構(gòu)(community structure)；最后，對(duì)團(tuán)體結(jié)構(gòu)進(jìn)行統(tǒng)計(jì)，并計(jì)算出團(tuán)體結(jié)構(gòu)的子句覆蓋率和變?cè)采w率，分析子句、變?cè)獙?duì)團(tuán)體結(jié)構(gòu)的影響大小。
　　實(shí)驗(yàn)結(jié)果發(fā)現(xiàn)，在SAT實(shí)例圖結(jié)構(gòu)表示中，存在著連通子圖，連通子圖之間的子句、變?cè)峭耆珱]有關(guān)聯(lián)的，這就將SAT實(shí)例分為完全獨(dú)立的子SAT實(shí)例，從而減小算例的復(fù)雜性。另一方面在實(shí)驗(yàn)中，團(tuán)體的變?cè)采w率在