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

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

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