基于分治的布爾可滿足性判定.pdf

1、SAT是最著名的NPC問(wèn)題。NPC類問(wèn)題有兩方面的特性，首先，這類問(wèn)題的解可以在多項(xiàng)式時(shí)間復(fù)雜度內(nèi)得到驗(yàn)證。其次，其它NP問(wèn)題可以在多項(xiàng)式時(shí)間內(nèi)轉(zhuǎn)換為NPC問(wèn)題來(lái)求解。因此，SAT判定技術(shù)的研究具有重要的理論意義。
　　SAT判定技術(shù)還具有很大的實(shí)用價(jià)值。它可以應(yīng)用到包括人工智能規(guī)劃、模型分析、定理證明、軟件驗(yàn)證和軟件測(cè)試、軟件發(fā)布中的包管理等領(lǐng)域。在電子設(shè)計(jì)自動(dòng)化中，SAT可用于電路的邏輯綜合、布爾匹配、電路等價(jià)性驗(yàn)證、模型檢驗(yàn)

2、、自動(dòng)測(cè)試用例生成、FPGA的布局布線、設(shè)計(jì)調(diào)試與診斷等。
　　本文研究SAT判定問(wèn)題，SAT判定問(wèn)題的時(shí)間復(fù)雜度是指數(shù)階的，這意味著如果問(wèn)題的規(guī)模較大時(shí)，要完成SAT判定會(huì)非常困難。
　　研究利用分治的思想，通過(guò)將復(fù)雜的SAT的判定問(wèn)題劃分為多個(gè)規(guī)模更小的子問(wèn)題來(lái)求解，在劃分代價(jià)較小的情況下，利用這一方法來(lái)降低可滿足性判定的復(fù)雜度。通過(guò)系統(tǒng)深入的理論分析和實(shí)驗(yàn)研究，取得了如下創(chuàng)新性成果：
　　提出了CNF形式的布爾公

3、式的子句組劃分的概念，并證明了布爾公式的可滿足性問(wèn)題可以轉(zhuǎn)化為子句組的可滿足性問(wèn)題來(lái)求解。給出了一種從CNF公式產(chǎn)生子句組劃分，以及利用子句組劃分來(lái)進(jìn)行SAT判定的方法。對(duì)于不能直接產(chǎn)生子句組劃分的公式，提出利用聚類方法，將子句聚類成多個(gè)簇，把包含共同變量多的子句聚類到同一個(gè)簇，包含共同變量少的子句聚類到不同的簇，將不同簇之間的共同變量作為割變量，通過(guò)對(duì)每個(gè)簇單獨(dú)判定，必要時(shí)再判斷割變量的取值是否沖突來(lái)判定公式的可滿足性。
　　由

4、于傳統(tǒng)的聚類方法并不能很好地適應(yīng)CNF子句的聚類要求，因此本文針對(duì)CNF公式的特點(diǎn)，提出一種兩階段的聚類方法，先用基于連接的方法來(lái)產(chǎn)生初始聚類，在一定程上避免聚類的局部最優(yōu)性，然后再用基于簇間相似度進(jìn)行合并的方法來(lái)生成最終的聚類結(jié)果。算法的第一階段通過(guò)指定聚類結(jié)果簇與原始簇個(gè)數(shù)的比值來(lái)確定生成的簇的個(gè)數(shù)，第二階段則通過(guò)相似度閾值來(lái)確定何時(shí)終止聚類，因此無(wú)需指定最終生成的簇的個(gè)數(shù)。
　　在聚類完成之后，如果要消去所有簇之間的共同變量

5、，將所有的簇都劃分開(kāi)，在某些情況下，由于公共變量太多，可能需要付出太大的代價(jià)。為解決這一問(wèn)題，本文提出將聚類結(jié)果中的簇作為頂點(diǎn)，用簇間的公共變量來(lái)標(biāo)記邊，將聚類結(jié)果變換成一個(gè)無(wú)向圖，然后利用無(wú)向圖最小割的方法來(lái)尋找將簇劃分成兩組的最小割變量集，以產(chǎn)生子句組劃分。
　　在某些情況下，將問(wèn)題變換為CNF公式，可能會(huì)導(dǎo)致一些結(jié)構(gòu)信息的丟失。針對(duì)組合電路的等價(jià)性驗(yàn)證問(wèn)題和AIG電路的特點(diǎn)，本文提出一種方法，直接在電路上通過(guò)電路的特點(diǎn)進(jìn)行推