應(yīng)用不可滿足子式的解碼電路綜合優(yōu)化方法*

張建民，黎鐵軍，馬柯帆，肖立權(quán)

(國(guó)防科技大學(xué) 計(jì)算機(jī)學(xué)院， 湖南 長(zhǎng)沙 410073)

?

應(yīng)用不可滿足子式的解碼電路綜合優(yōu)化方法*

張建民，黎鐵軍，馬柯帆，肖立權(quán)

(國(guó)防科技大學(xué) 計(jì)算機(jī)學(xué)院， 湖南 長(zhǎng)沙 410073)

解釋布爾公式不可滿足的原因在很多領(lǐng)域都具有實(shí)際的應(yīng)用需求，而最小不可滿足子式能夠?yàn)橹T如電路的自動(dòng)綜合等應(yīng)用領(lǐng)域中的不可滿足原因提供最精確的解釋。因此，將兩種能夠高效求解最小不可滿足子式的算法——分支-限界算法與貪心遺傳算法，集成到解碼電路的自動(dòng)綜合工具中。采用通信領(lǐng)域的標(biāo)準(zhǔn)編碼電路作為測(cè)試集，將兩種算法進(jìn)行對(duì)比。實(shí)驗(yàn)結(jié)果表明，在運(yùn)行時(shí)間與每秒剔除的短句數(shù)方面，貪心遺傳算法優(yōu)于分支-限界算法；不可滿足子式在解碼電路的自動(dòng)綜合過程中發(fā)揮重要作用。

電路綜合；形式化方法；可滿足性求解；不可滿足子式

在超大規(guī)模集成(Very Large Scale Integrated， VLSI)電路芯片中，通常都會(huì)設(shè)計(jì)各種各樣的編碼和解碼電路，尤其是在與通信相關(guān)的芯片設(shè)計(jì)過程中，往往會(huì)遇到很多非常復(fù)雜的編碼與解碼電路。編碼電路通常根據(jù)某種規(guī)則將原始數(shù)據(jù)編碼或產(chǎn)生校驗(yàn)碼，常見的包括循環(huán)冗余校驗(yàn)(Cyclic Redundancy Code，CRC)或糾錯(cuò)碼(Error Correction Code，ECC)，而解碼電路根據(jù)校驗(yàn)碼和原始數(shù)據(jù)判定接收的數(shù)據(jù)是否正確。這些電路需要消耗設(shè)計(jì)者大量的時(shí)間來進(jìn)行驗(yàn)證，那么，能否只設(shè)計(jì)與驗(yàn)證編碼電路，而后通過一種自動(dòng)化的方法來產(chǎn)生正確的解碼電路，從而降低設(shè)計(jì)者的工作量？因此，產(chǎn)生了自動(dòng)對(duì)偶綜合工具[1]。自動(dòng)對(duì)偶綜合的基本思路是：給出一個(gè)已驗(yàn)證的編碼電路，通過形式化的方法自動(dòng)綜合出一個(gè)功能正確的解碼電路。對(duì)偶綜合工具通過分析特定編碼電路的狀態(tài)空間，自動(dòng)產(chǎn)生相應(yīng)的解碼電路，避免設(shè)計(jì)人員將時(shí)間花費(fèi)在設(shè)計(jì)解碼器上，從而降低芯片設(shè)計(jì)的風(fēng)險(xiǎn)，并加速設(shè)計(jì)進(jìn)程。而在對(duì)偶綜合工具中，使用不可滿足子式求解器，移除冗余短句以削減狀態(tài)空間，是加快整體運(yùn)行速度的關(guān)鍵。

自動(dòng)對(duì)偶綜合工具的基本流程是：以編碼電路的寄存器傳輸級(jí)(Register Transfer Level，RTL) Verilog代碼和工具的參數(shù)配置作為輸入，首先采用Verilog語(yǔ)法分析器將設(shè)計(jì)轉(zhuǎn)換為內(nèi)部的中間表示，而后在狀態(tài)空間中進(jìn)行搜索，通過合取范式(Conjunctive Normal Form，CNF)產(chǎn)生器得到布爾公式；再調(diào)用一種高效的SAT求解器——zChaff求解器，判定公式的可滿足性。若可滿足，則算法繼續(xù)搜索；否則采用不可滿足子式求解器提取最小不可滿足子式，并將該子式作為輸入，反向抽取出解碼電路的RTL代碼。

布爾不可滿足子式求解器是自動(dòng)對(duì)偶綜合工具的重要組成部分。由于不可滿足子式越小，越有利于反向電路提取，因此在自動(dòng)對(duì)偶綜合工具中主要集成了求解最小不可滿足子式的算法。而在當(dāng)前求解最小不可滿足子式的算法中，分支-限界算法[2]與貪心遺傳算法[3]是最高效的兩種算法，二者的相同之處是都基于布爾公式的極大可滿足性與極小不可滿足性之間的關(guān)系，區(qū)別在于優(yōu)化策略，前者采用確定性最優(yōu)化的分支-限界算法，后者采用近似最優(yōu)化的貪心遺傳算法。

1 不可滿足子式的定義

CNF公式的基本消解規(guī)則為：

表示為[(A∨x)∧(B∨x)](A∨B)，其中x是一個(gè)變?cè)?，叫作消解元，A與B表示若干個(gè)文字的析取，(A∨x)與(B∨x)稱為消解母式，而結(jié)果短句(A∨B)稱為消解式。短句(x)與(x)的消解式為空短句。每次應(yīng)用消解規(guī)則產(chǎn)生消解式叫作一個(gè)消解步驟。一系列的消解步驟，其中每一步都使用前面步驟產(chǎn)生的消解式或原始公式中的短句作為當(dāng)前的消解短句，稱為消解序列。

引理1 當(dāng)且僅當(dāng)存在有限個(gè)消解步驟且最終產(chǎn)生的消解式為空短句時(shí)，CNF公式是不可滿足的。

定義1(不可滿足子式) 給定一個(gè)不可滿足公式φ，當(dāng)且僅當(dāng)ψ是不可滿足的且ψφ時(shí)，ψ是公式φ的一個(gè)不可滿足子式。

定義2(極小不可滿足子式) 給定不可滿足公式φ的一個(gè)不可滿足子式ψ，當(dāng)且僅當(dāng)φψ且φ是可滿足的時(shí)，ψ是極小不可滿足子式。

對(duì)于CNF公式來說，如果一個(gè)不可滿足子式是不可約的，即它的所有真子集都是可滿足的，那么它是極小不可滿足子式。

定義3(最小不可滿足子式) 給定一個(gè)不可滿足公式φ以及φ的所有不可滿足子式構(gòu)成的集合：{ψ1,ψ2, …,ψj}。那么當(dāng)且僅當(dāng)ψi∈ {ψ1,ψ2, …,ψj}，1≤i≤j，使得時(shí)，ψk∈{ψ1,ψ2, …,ψj}是最小不可滿足子式。

根據(jù)定義3，最小不可滿足子式是公式的所有不可滿足子式中長(zhǎng)度最小的，即所包含的短句數(shù)最少。所有不可滿足的布爾公式都至少包含一個(gè)最小不可滿足子式。相對(duì)于不可滿足子式或極小不可滿足子式，最小不可滿足子式往往包含一些簡(jiǎn)單消解規(guī)則所不能剔除的冗余短句，因此最小不可滿足子式的求解難度更大，算法復(fù)雜度更高，但是對(duì)于應(yīng)用的優(yōu)化效果最佳。相對(duì)于求解極小不可滿足子式的研究來講，近年來關(guān)于如何求解最小不可滿足子式的研究工作較少。

2 不可滿足子式的求解算法

近年來，相繼涌現(xiàn)出了許多求解布爾不可滿足子式的研究成果。21世紀(jì)初，自從融合沖突學(xué)習(xí)機(jī)制等啟發(fā)式方法的DPLL(Davis-Putnam-Logemann-Loveland)算法出現(xiàn)之后，SAT求解器得到了飛速的發(fā)展，因此，基于SAT求解器的不可滿足子式求解方法也逐漸成了研究的主流方向。zCore[4]是一種基于高效SAT求解器產(chǎn)生的消解悖論來提取不可滿足子式的算法，但是其結(jié)果只是小的而非極小不可滿足子式。另外一個(gè)僅能求解不可滿足子式的算法是AMUSE[5]，該算法在增加選擇變?cè)墓缴贤ㄟ^增強(qiáng)DPLL過程搜索不可滿足子式。Lynce等[6]提出了一種使用SAT求解器來窮盡搜索公式的全部空間，從而得到最小不可滿足子式的算法。

Timmer算法[7]通過證明短句蘊(yùn)含圖中的一個(gè)結(jié)點(diǎn)等價(jià)于一組短句，而后刪除該組短句，不斷循環(huán)直到產(chǎn)生不可滿足子式。Dershowitz等[8]利用SAT求解器產(chǎn)生的消解悖論，移除一個(gè)初始短句及其導(dǎo)致的所有沖突短句，通過檢驗(yàn)剩余子公式的可滿足性來確定該短句是否屬于不可滿足子式。Maaren等[9]基于Brouwer不動(dòng)點(diǎn)定理來求解極小不可滿足子式，將判定公式的不可滿足性轉(zhuǎn)換為從Pareto最優(yōu)規(guī)則中找到一個(gè)短句的子集或并集的可能性。東南大學(xué)陳振宇等[10]提出了一種基于消解的極小不可滿足子式求解算法，并應(yīng)用于模型檢驗(yàn)。吉林大學(xué)趙相福等[11]則提出了產(chǎn)生所有的極小不可滿足子式集合的算法。

Nadel[12]提出了兩種基于消解的極小不可滿足子式求解算法，但在算法超時(shí)時(shí)，則僅得到非極小不可滿足子式。Marques-Silva等[13]提出了兩種求解極小不可滿足子式的算法，第一種算法將運(yùn)行時(shí)調(diào)用SAT求解器的次數(shù)最小化，第二種算法在之前工作的基礎(chǔ)上集成了很多新的優(yōu)化技術(shù)。Ryvchin等[14]在消解算法[12]的基礎(chǔ)上提出了7種優(yōu)化技術(shù)，實(shí)驗(yàn)表明其能夠減少55%的運(yùn)行時(shí)間以及73%的不可滿足子式的短句數(shù)。Chen等[15]提出了通過求解不可滿足子式來加速布爾公式分解的兩種優(yōu)化技術(shù)。Belov等[16]引入了迭代模型旋轉(zhuǎn)的技術(shù)，該技術(shù)能夠有效地提高求解不可滿足子式的效率。該作者還借鑒了求解不可滿足子式的多種優(yōu)化技術(shù)，用于求解公式的最小等價(jià)子式[17]。

Liffiton等[18]提出一種新的算法用于求解多個(gè)不可滿足子式，能適用于每種約束系統(tǒng)。Nadel等[19]將模型旋轉(zhuǎn)技術(shù)應(yīng)用于基于消解的極小不可滿足子式求解方法中，并提出了eager旋轉(zhuǎn)和路徑增強(qiáng)技術(shù)以提高求解效率。Lagniez等[20]引入基于假設(shè)的文字參數(shù)化增量式SAT求解技術(shù)，用于加速不可滿足子式的提取過程。Marques-Silva等[21]提出了基于布爾公式單調(diào)謂詞的不可滿足子式求解算法，并且通過實(shí)驗(yàn)表明，該方法屬于當(dāng)前最優(yōu)算法。Belov等[22]引入了沖突驅(qū)動(dòng)的短句學(xué)習(xí)SAT求解器中的短句證明技術(shù)，用于求解極小不可滿足子式的剪枝過程。在SAT′14上，有學(xué)者[23]提出了偏好極小不可滿足子式與極小正確子集的概念，并集成已有的優(yōu)化剪枝技術(shù)，給出了求解算法。

下面簡(jiǎn)要地介紹一下當(dāng)前兩種最優(yōu)的最小不可滿足子式求解算法：分支-限界算法與貪心遺傳算法。Liffiton等[2]提出了一種求解最小布爾不可滿足子式的分支-限界算法，該算法利用極大可滿足性反復(fù)產(chǎn)生不可滿足子式的上界與下界，并在特定的子公式上分支，從而得到最小不可滿足子式。該算法能夠處理實(shí)際應(yīng)用中較大規(guī)模的問題，例如DaimlerChrysler測(cè)試集。該算法的優(yōu)點(diǎn)是能得到準(zhǔn)確的最小不可滿足子式，不足之處是效率都相對(duì)不高。張建民等[3]證明了最小不可滿足性與極大可滿足性之間的關(guān)系，并且基于二者的關(guān)系，提出一種貪心遺傳算法解決從公式中提取最小不可滿足子式的問題。算法的主要過程是：根據(jù)最小不可滿足性與極大可滿足性之間的關(guān)系，首先利用SAT求解器，通過增加短句選擇因子與限界約束的方式，提取布爾公式的所有極大可滿足子式；而后計(jì)算極大可滿足子式補(bǔ)集的最小碰集，從而得到最小不可滿足子式。該算法的優(yōu)勢(shì)是求解效率高，不足之處是對(duì)于某些公式，僅能得到近似而非精確的最小不可滿足子式。

3 基于不可滿足子式的解碼電路綜合優(yōu)化方法

在VLSI電路中，尤其是在與通信相關(guān)的芯片設(shè)計(jì)過程中，往往會(huì)遇到很多非常復(fù)雜的編碼與解碼電路。這些電路需要滿足許多特定的編碼要求，如直流均衡、游程、校驗(yàn)、最大包長(zhǎng)度、包間間隔、對(duì)時(shí)鐘和數(shù)據(jù)偏斜的容忍度等，而這些要求在不同的應(yīng)用環(huán)境中又有著完全不同的側(cè)重點(diǎn)。使用單一IP核無(wú)法在所有的情況下均得到最優(yōu)化的設(shè)計(jì)。滿足這些編碼要求的編碼器和解碼器需要消耗設(shè)計(jì)者大量的時(shí)間進(jìn)行驗(yàn)證，那么，能否只設(shè)計(jì)與驗(yàn)證編碼電路，而后通過一種自動(dòng)化的方法來產(chǎn)生正確的解碼電路，從而降低設(shè)計(jì)者的工作量？因此，產(chǎn)生了自動(dòng)對(duì)偶綜合的概念。自動(dòng)對(duì)偶綜合的基本思路是：給出一個(gè)經(jīng)過驗(yàn)證的編碼電路，通過形式化的方法自動(dòng)綜合出一個(gè)功能正確的解碼電路。

通常，絕大多數(shù)的編碼器都可以用一個(gè)簡(jiǎn)單的模型建模，稱之為DELAY-LENGTH模型。該模型的兩個(gè)參數(shù)構(gòu)成一個(gè)二元組，d和l分別表示該模型的延時(shí)和數(shù)據(jù)粒度。其直觀描述為：在輸入端，任意一個(gè)長(zhǎng)度為l個(gè)周期的數(shù)據(jù)單元，在d個(gè)周期之后，將在輸出端產(chǎn)生長(zhǎng)度為l的輸出。一方面，該模型允許一個(gè)輸入在不同的初始狀態(tài)情況下產(chǎn)生不同的輸出。這與通信系統(tǒng)中為了追求直流平衡而采用的parity機(jī)制和冗余編碼機(jī)制是一致的，而且并不妨礙正確的譯碼。而另一方面，該模型不允許兩個(gè)不同的輸入產(chǎn)生相同的輸出，否則將無(wú)法完成正確的譯碼。

自動(dòng)對(duì)偶綜合的原理如圖1所示。假設(shè)編碼電路表示為C，解碼電路表示為C，那么可以將編碼電路C沿時(shí)間軸展開n個(gè)時(shí)鐘周期，構(gòu)成一個(gè)新的電路Cn：Cn=C×C×…×C。根據(jù)電路Cn，構(gòu)造一個(gè)與其完全相同的電路拷貝，記為。定義一個(gè)算子?：F=Cn?(表示兩個(gè)電路的輸入不同，輸出相同，構(gòu)成的電路記為F)。根據(jù)一個(gè)給定的二元組，可以將編碼電路C展開d+l個(gè)時(shí)鐘周期，構(gòu)成電路Cd+l；構(gòu)造另外一個(gè)與Cd+l完全相同的電路拷貝，記為。根據(jù)算子?的定義，得到電路F=Cd+l?。

圖1 自動(dòng)對(duì)偶綜合的基本原理Fig.1 Principle of automatic decoder synthesis

圖2給出了自動(dòng)對(duì)偶綜合工具的結(jié)構(gòu)框圖，其中粗框表示即為本文所實(shí)現(xiàn)的布爾不可滿足子式求解器。由于不可滿足子式越小，越有利于反向電路提取，因此在自動(dòng)對(duì)偶綜合工具中主要集成了求解最小不可滿足子式的分支-限界算法與貪心遺傳算法。自動(dòng)對(duì)偶綜合工具的基本流程是：以編碼電路的RTL Verilog代碼和工具的參數(shù)配置作為輸入，首先采用Verilog語(yǔ)法分析器將設(shè)計(jì)轉(zhuǎn)換為內(nèi)部的中間表示，而后在狀態(tài)空間中進(jìn)行搜索，通過CNF產(chǎn)生器得到布爾公式，利用zCahff求解器判定公式的可滿足性。若可滿足，則繼續(xù)搜索；否則采用不可滿足子式求解器提取最小不可滿足子式，并將該子式作為輸入，反向抽取出解碼電路的RTL代碼。

圖2 自動(dòng)對(duì)偶綜合工具的結(jié)構(gòu)Fig.2 Architecture of automatic decoder synthesis tool

4 實(shí)驗(yàn)結(jié)果對(duì)比與分析

為了驗(yàn)證不可滿足子式求解算法在電路自動(dòng)對(duì)偶綜合中的作用，以業(yè)界普遍采用的、遵循IEEE802.3ae標(biāo)準(zhǔn)的編碼器電路作為實(shí)例。IEEE802.3ae是IEEE于2002年發(fā)布的關(guān)于數(shù)據(jù)通信的IEEE802.3以太網(wǎng)協(xié)議與幀格式的一組協(xié)議規(guī)范，該標(biāo)準(zhǔn)定義了信號(hào)速率從1 Mb/s到1000 Mb/s的多種介質(zhì)類型和技術(shù)。物理編碼子層(Physical Coding Sublayer， PCS)是物理層實(shí)現(xiàn)的一個(gè)部件，PCS所使用的編碼技術(shù)為8B/10B，該編碼技術(shù)將報(bào)文編碼為10位寬度的數(shù)據(jù)組，或者將10位的數(shù)據(jù)組解碼為有效報(bào)文。

針對(duì)業(yè)界常用的PCS 8B/10B編碼電路，當(dāng)二元組的值d=1，l=1時(shí)，自動(dòng)對(duì)偶綜合工具能夠得到不可滿足的DIMACS CNF格式的布爾公式，稱為PCS_d1l1.cnf，如圖3(a)所示，該公式包含2189個(gè)變?cè)?103個(gè)短句。當(dāng)d=2，l=1時(shí)，對(duì)偶綜合工具得到的不可滿足的CNF公式稱為PCS_d2l1.cnf，該公式包含3399個(gè)變?cè)?0 853個(gè)短句，如圖3(b)所示。將d和l分別取值1,2,3時(shí)，得到另外7個(gè)公式，分別命名為：PCS_d1l2.cnf，PCS_d1l3.cnf，PCS_d2l2.cnf，PCS_d3l1.cnf，PCS_d3l2.cnf，PCS_d2l3.cnf和PCS_d3l3.cnf。當(dāng)d≥4或l≥4時(shí)，由于狀態(tài)空間過于龐大，解碼電路的自動(dòng)綜合工具無(wú)法得到不可滿足公式。

基于上述自動(dòng)對(duì)偶綜合工具產(chǎn)生的9個(gè)公式，分別采用分支-限界算法[2]以及貪心遺傳算法[3]求解它們的最小不可滿足子式。兩種算法的運(yùn)行時(shí)限都設(shè)置為1800 s。實(shí)驗(yàn)環(huán)境是主頻為2.5 GHz的雙核Athlon CPU，內(nèi)存2 GB，操作系統(tǒng)為L(zhǎng)inux的機(jī)器。

表1給出了分支-限界算法與貪心遺傳算法在PCS編碼電路上的結(jié)果。表中的第二列與第三列分別表示公式所包含的變?cè)獢?shù)與短句數(shù)；兩算法下的第一、二、三列分別表示算法各自的運(yùn)行時(shí)間、得到的最小不可滿足子式長(zhǎng)度以及單位時(shí)間移除的短句數(shù)。最后一列以百分比的形式表示最小不可滿足子式所包含的短句數(shù)占公式總短句數(shù)的比例。

從表1可以看出，貪心遺傳算法在運(yùn)行時(shí)間方面優(yōu)于分支-限界算法，只有分支-限界算法運(yùn)行時(shí)間的52%～64%。另外，雖然貪心遺傳算法僅得到了近似最小不可滿足子式，但其只比分支-限界算法所求的最小不可滿足子式多約4～8個(gè)短句。根據(jù)每秒剔除短句數(shù)nps的概念可得其計(jì)算公式是：nps= (NumLen)/Time，其中Num表示公式的短句數(shù)，Len表示不可滿足子式的長(zhǎng)度，即所包含的短句數(shù)，Time表示算法的運(yùn)行時(shí)間，單位為秒。從nps列可以看出，貪心遺傳算法每秒移除的短句數(shù)可以達(dá)到分支-限界算法的1.6～1.9倍。上述實(shí)驗(yàn)結(jié)果表明，貪心遺傳算法雖然在求解最小不可滿足子式的長(zhǎng)度方面犧牲了一點(diǎn)精度，但在算法運(yùn)行時(shí)間上取得了很大的優(yōu)勢(shì)，表明其同時(shí)兼顧算法效率與結(jié)果質(zhì)量，且在單位時(shí)間內(nèi)剔除的短句數(shù)要顯著高于分支-限界算法，因此在眾多的實(shí)際應(yīng)用中，貪心遺傳算法要比分支-限界算法更加高效、更加實(shí)用。

(a) DIMACS公式PCS_d1l1.cnf(部分)(a) PCS_d1l1.cnf in DIMACS format (part) (b) DIMACS公式PCS_d2l1.cnf(部分)(b) PCS_d2l1.cnf in DIMACS format (part)圖3 DIMACS公式PCS_d1l1.cnf與PCS_d2l1.cnf (部分)Fig.3 PCS_d1l1.cnf and PCS_d2l1.cnf in DIMACS format (part)

表1 分支-限界算法與貪心遺傳算法的實(shí)驗(yàn)對(duì)比

從表1的最后一列可以看出，貪心遺傳算法與分支-限界算法所求解的最小不可滿足子式包含的短句非常少，僅占原始公式總短句數(shù)的10%～21%。這表明，在自動(dòng)對(duì)偶綜合工具中，通過求解最小不可滿足子式能夠大大簡(jiǎn)化狀態(tài)空間，減小搜索范圍，從而使得綜合工具更加易于從編碼電路中自動(dòng)地提取PCS解碼電路。通過實(shí)驗(yàn)說明，最小不可滿足子式能夠?yàn)橹T如電路的自動(dòng)綜合等多種應(yīng)用領(lǐng)域中的不可滿足原因提供最精確的解釋，最大限度地剔除無(wú)關(guān)因素，從而顯著地加速應(yīng)用的運(yùn)行效率。

5 結(jié)論

解碼電路的自動(dòng)綜合方法是不可滿足子式的典型應(yīng)用。由于不可滿足子式越小，越能加速解碼電路的提取，因此，將兩種能夠高效求解最小不可滿足子式的算法——分支-限界算法與貪心遺傳算法，集成到電路綜合工具中。采用通信領(lǐng)域最典型的IEEE802.3ae標(biāo)準(zhǔn)編碼電路作為測(cè)試集，將兩種算法進(jìn)行了對(duì)比實(shí)驗(yàn)。結(jié)果表明，在運(yùn)行時(shí)間與每秒剔除的短句數(shù)方面，貪心遺傳算法優(yōu)于分支-限界算法。并且通過該實(shí)驗(yàn)表明，最小不可滿足子式求解器能夠顯著地提高解碼電路自動(dòng)綜合工具的效率。

References)

[1] Shen S Y, Qin Y, Wang K, et al. Synthesizing complementary circuits automatically[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2010, 29(8): 1191-1202.

[2] Liffiton M H, Mneimneh M N, Lynce I, et al. A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas[J]. Constraints, 2009, 14(4): 415.

[3] 張建民, 沈勝宇, 李思昆. 最小布爾不可滿足子式的求解算法[J]. 電子學(xué)報(bào), 2009, 37(3): 993-999.

ZHANG Jianmin, SHEN Shengyu, LI Sikun. Algorithms for deriving minimum unsatisfiable boolean subformulae[J]. Acta Electronica Sinica, 2009, 37(3): 993-999. (in Chinese)

[4] Zhang L T, Malik S. Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications[C] //Proceedings of Design, Automation and Test in Europe Conference(DATE′03), 2003: 10880-10885.

[5] Oh Y, Mneimneh M N, Andraus Z S, et al. AMUSE: a minimally-unsatisfiable subformula extractor[C] //Proceedings of the 41st Design Automation Conference(DAC′04), 2004: 518-523.

[6] Lynce I, Marques-Silva J. On computing minimum unsatisfiable cores[C] //Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing(SAT′04), 2004: 305-310.

[7] Gershman R, Koifman M, Strichman O. Deriving small unsatisfiable cores with dominator[C] //Proceedings of the 18th International Conference on Computer Aided Verification(CAV′06), 2006: 109-122.

[8] Dershowitz N, Hanna Z, Nadel A. A scalable algorithm for minimal unsatisfiable core extraction[C] //Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing(SAT′06), 2006: 36-41.

[9] van Maaren H, Wieringa S. Finding guaranteed MUSes fast[C] // Proceedings of 11th International Conference on Theory and Applications of Satisfiability Testing(SAT′08), 2008: 291-304.

[10] 陳振宇, 徐寶文, 周從華. 一種基于消解的變量極小不可滿足子公式的提取方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2008, 45(z1): 43-47.

CHEN Zhenyu, XU Baowen, ZHOU Conghua. A resolution-based approach for extracting variable minimal unsatisfiable sub-formulas[J]. Journal of Computer Research and Development, 2008, 45(z1): 43-47. (in Chinese)

[11] 趙相福, 歐陽(yáng)丹彤. 使用SAT求解器產(chǎn)生所有極小沖突部件集[J]. 電子學(xué)報(bào), 2009, 37 (4): 804-810.

ZHAO Xiangfu, OUYANG Dantong. Deriving all minimal conflict sets using satisfiability algorithms[J]. Acta Electronica Sinica, 2009, 37(4): 804-810. (in Chinese)

[12] Nadel A. Boosting minimal unsatisfiable core extraction[C] // Proceedings of the 10th International Conference on Formal Methods in Computer Aided Design (FMCAD′10), 2010: 221-229.

[13] Marques-Silva J, Lynce I. On improving MUS extraction algorithms[C] //Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing(SAT′11), 2011: 159-173.

[14] Ryvchin V, Strichman O. Faster extraction of high-level minimal unsatisfiable cores[C] //Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing(SAT′11), 2011: 174-187.

[15] Chen H, Marques-Silva J. Improvements to satisfiability-based boolean function bi-decomposition[C] //Proceedings of the 19th International Conference on VLSI and System-on-Chip (VLSI-SoC′11), 2011: 52-72.

[16] Belov A, Lynce I, Marques-Silva J. Towards efficient MUS extraction[J]. Journal AI Communications, 2012, 25(2): 97-116.

[17] Belov A, Janota M, Lynce I, et al. On computing minimal equivalent subformulas[C]// Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming(CP′12), 2012: 158-174.

[18] Liffiton M H, Malik A. Enumerating infeasibility: finding multiple MUSes quickly[C]// Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 2013: 160-175.

[19] Nadel A, Ryvchin V, Strichman O. Efficient MUS extraction with resolution[C]// Proceedings of 13th International Conference Formal Methods in Computer Aided Design(FMCAD′13), 2013: 197-200.

[20] Lagniez J M, Biere A. Factoring out assumptions to speed up MUS extraction[C] //Proceedings of 16th International Conference on Theory and Applications of Satisfiability Testing(SAT′13), 2013: 276-292.

[21] Marques-Silva J, Janota M, Belov A. Minimal sets over monotone predicates in Boolean formulae[C] //Proceedings of the 25th International Conference on Computer Aided Verification(CAV′13), 2013: 592-607.

[22] Belov A, Heule M J H, Marques-Silva J. MUS extraction using clausal proofs[C] //Proceedings of 17th International Conference on Theory and Applications of Satisfiability Testing(SAT′14), 2014: 48-57.

[23] Marques-Silva J, Previti A. On computing preferred MUSes and MCSes[C] //Proceedings of 17th International Conference on Theory and Applications of Satisfiability Testing(SAT′14), 2014: 58-74.

Optimization method of decoding circuits′ synthesis using unsatisfiable subformulas

ZHANG Jianmin, LI Tiejun, MA Kefan, XIAO Liquan

(College of Computer, National University of Defense Technology, Changsha 410073, China)

Explaining the causes of unsatisfiability of the Boolean formulas has many real applications in various fields. The minimum unsatisfiable subformulas can provide most accurate explanations for the causes of infeasibility in many application fields such as the automatic circuits' synthesis. Therefore, two best algorithms of extracting the minimum unsatisfiable subformulas, respectively called the branch-and-bound algorithm and greedy genetic algorithm, were integrated into the automatic synthesis tool of decoding circuits. Adopting the standard encoding circuits in communication fields as the benchmarks, the study compared and analyzed the two algorithms. The experimental results show that the greedy genetic algorithm outperforms the branch-and-bound algorithm on runtime and removed clauses per second. The results also show that the unsatisfiable subformulas play an important role in the process of synthesizing automatically the decoding circuits.

circuit synthesis; formal method; satisfiability solving; unsatisfiable subformula

10.11887/j.cn.201605001

http://journal.nudt.edu.cn

2015-11-17

國(guó)家自然科學(xué)基金資助項(xiàng)目(61103083，61133007)；國(guó)家重點(diǎn)研發(fā)計(jì)劃資助項(xiàng)目(2016YFB0200203)

張建民(1979—)，男，山西平遙人，副研究員，博士，Email: jmzhang@nudt.edu.cn

TP391

A

1001-2486(2016)05-001-06