中山大學(xué)邏輯與認(rèn)知研究所 周 進(jìn) 趙希順

邏輯器件可分類兩大類：固定邏輯器件和可編程邏輯器件。固定邏輯器件中的電路是永久性的，其硬件邏輯結(jié)構(gòu)和連接方式固定不變。而可編程邏輯器件（FPGA，CPLD等）內(nèi)部連接模式和邏輯結(jié)構(gòu)可以根據(jù)不同的需要改變，從而可以實現(xiàn)多種不同的功能。所以，此類器件能夠為客戶提供范圍廣泛的具有多種邏輯能力、速度和電壓特性的標(biāo)準(zhǔn)成品部件。

可編程硬件算法研究的發(fā)展是和硬件水平的發(fā)展密不可分的?？删幊逃布侵缸钤绲挠布删幊趟惴ǖ母拍钍荊.Estrin在1960年左右提出的[1]，但由于主要以分立器件為硬件平臺，而集成電路也尚在初期，因此并未得到更多研究和應(yīng)用的支持。從1990年開始，超過10K門級的可編程邏輯器件FPGA（其典型結(jié)構(gòu)如圖一所示）的出現(xiàn)，使得硬件可編程邏輯算法的研究進(jìn)入了蓬勃發(fā)展的時期[2]，其應(yīng)用主要分為三種：1、硬件設(shè)計模擬；2、快速硬件成樣；3、硬件算法研究。而其中硬件算法研究是基于FPGA硬件并行處理能力，已經(jīng)在密碼學(xué)，圖像和信號處理領(lǐng)域取得了很多成果。自1997年后，隨著FPGA進(jìn)入到了百萬門級的水平，硬件可編程邏輯能力上升到了一個新的高度，基于硬件可編程邏輯的高難度算法的實現(xiàn)與研究也受到越來愈多的關(guān)注。其中，基于FPGA的可滿足性問題（SAT問題）的算法研究逐漸成為研究的熱點[7-14]。

SAT問題是邏輯學(xué)的一個基本問題，也是當(dāng)今計算機科學(xué)和人工智能研究的核心問題。工程技術(shù)、軍事、工商管理、交通運輸及自然科學(xué)研究中的許多重要問題，如程控電話的自動交換、大型數(shù)據(jù)庫的維護(hù)、大規(guī)模集成電路的自動布線、軟件自動開發(fā)、機器人動作規(guī)劃等，都可轉(zhuǎn)化成SAT問題。可滿足性SAT問題同時也是第一個被證明的NP-Complete問題，目前解決SAT問題已有的完全算法的運行時間呈指數(shù)增長。因此，基于FPGA(如圖一)對SAT算法加速的研究，具有很大的理論和應(yīng)用價值，同時也有助于尋找優(yōu)化其他復(fù)雜計算的方法。

一、問題定義

對于命題公式Y(jié)，如果存在對Y中變量的賦值，使得Y在該賦值下的真值為1，則稱Y是可滿足的?？蓾M足性問題(SAT問題)是判定一個任意給定的命題公式是否可滿足的問題。眾所周知，任何命題邏輯公式都邏輯等價于一個合取范式（CNF-Conjunctive Normal Form）。合取范式即是子句的合取，而子句是文字(變元或其否定)的析取。

SAT算法可以分為完全算法(Complete)和不完全算法(Incomplete)算法兩大類。通過完全算法總是可以判斷公式是否可以滿足，盡管有可能計算時間是相當(dāng)長的。如Davis-Putnam 的DP算法[3]和廣泛用于電子電路測試向量生成的PODEM(Path-Oriented Decision Making) 算法[4]都是完全算法。不完全算法則是規(guī)定的時間內(nèi)尋找SAT問題的解，如果找到則說明可滿足，但找不到SAT的可滿足解不能作為SAT是否可滿足的依據(jù)。經(jīng)典的DP算法如下所示，通過遍歷變量空間的方式搜索滿足SAT的解。

圖二所示的是DP算法的例子。

隨著研究的深入，很多DP算法的優(yōu)化算法和技術(shù)涌現(xiàn)出來，其中有代表性的如GRASP(Generic search Algorithm for the Satisfiability Problem)算法中的non-chronological回溯技術(shù)[5]等。

二、研究進(jìn)展現(xiàn)狀和發(fā)展趨勢

基于可編程邏輯的SAT的算法研究分為兩個大的階段，前期（1996-2002）以實例型（Instance-Specified Solver）算法為標(biāo)志；后期（2002-至今）以應(yīng)用型（Application-Specified Solver）算法為標(biāo)志。

● 實例型（Instance-Specified Solver）算法：硬件結(jié)構(gòu)針對每一個實例進(jìn)行編譯配置然后計算的方式，每一個不同的實例對應(yīng)不同的硬件結(jié)構(gòu)。

● 應(yīng)用型（Application-specified solver）算法：硬件結(jié)構(gòu)針對應(yīng)用進(jìn)行一次編譯和配置然后計算，在同一個硬件機構(gòu)上對應(yīng)用中不同的實例進(jìn)行計算。

（1）實例型（Instance-Specified Solver）算法（1996-2002）

ⅰ)實例型硬件直接邏輯算法：Suyama et all（1996）

Suyama et al.[7]在1996年首次提出了實例型硬件直接邏輯算法（如圖三所示）。他首先將SAT實例CNF先轉(zhuǎn)換為3-SAT，然后由SFL Generator轉(zhuǎn)換為HDL語言，將其編譯下載后在FPGA固化為硬件邏輯。形成CNF的Clause邏輯計算模塊。通過在2N-1的空間用窮舉法或類似DP回溯算法搜索取值，對實例的可滿足型進(jìn)行求解。

該研究采用DIMACS(Center for Discrete Mathematics & Theoretical Computer Science)[15]的幾個實例在 Altera FLEX10K250 FPGA時鐘頻率10Hz的平臺上進(jìn)行了驗證。測試結(jié)果和在UltraSPARC-II/296MHz上的POSIT(Propositional satisfibility testbed)結(jié)果進(jìn)行了比較，速度可以達(dá)到1-10倍。但是其計算的速度的計算沒有包含F(xiàn)PGA編譯和配置的時間。

ⅱ)實例型硬件狀態(tài)機（FSM）DP算法：Zhong et al.(1999)

1999年Zhong et al.提出了如圖四所示DP算法的硬件可編程SAT算法[8]。SAT Clause編譯為FPGA硬件Deduction模塊和Implication模塊，以采用流水線結(jié)構(gòu)進(jìn)行計算。算法模型采用了如圖四所示的有限狀態(tài)機（FSM）的方式。

實驗通過多個FPGA互聯(lián)形成Xilinx FPGA硬件陣列進(jìn)行了驗證。和著名的軟件算法GRASP在Sun5/110MHz/64MB保護(hù)模式下比較，提高了一個數(shù)量級的速度，但該結(jié)果同樣未將硬件編譯和配置時間計入。

圖一 FPGA 的典型結(jié)構(gòu)

圖二 DP算法舉例

圖三 實例型硬件算法-直接邏輯計算

圖四 實例型硬件算法-有限狀態(tài)機

FSM的使用使得該算法可以有效利用DP的相關(guān)軟件算法中的技術(shù)如non chronological backtracking等。而且結(jié)構(gòu)具有可擴展性，對于大的SAT實例，可以采用互聯(lián)的FPGA陣列解決。該方法利用了FPGA的管道技術(shù)，提高了數(shù)據(jù)處理速度。但由于實例型算法編譯和硬件配置時間漫長，實用性不夠，同時運算中每個時鐘周期只有一個FSM激活，周期利用率低。

ⅲ)實例型硬件并行PODEM算法：Abromavici et al.(2000)

Abromavici et al.(2000)利用了電子電路測試中測試向量生成的常用算法，提出了如圖五所示的SAT實例型算法的新的思路[9]。他將CNF編譯成為對應(yīng)的PODEM電路形式，通過向前推導(dǎo)輸出模型（Forward model）和向后反推輸入模型（Backward model），進(jìn)行多路并行的推導(dǎo)，得到SAT問題的解。

實驗通過DIMACS部分實例在XC6264 FPGA，主頻3.5 MHz的平臺上進(jìn)行了驗證。和著名的軟件算法GRASP在Sun Ultra Sparc工作站1026Mb RAM和248MHz主頻下比較，未將硬件編譯和配置時間計入的情況下，提高了1.01-7000倍的速度。

ⅳ)實例型硬件混合算法：Dandalis et al.(2002)

Dandalis et al.首次提出了如圖六所示的軟硬件混合的算法，將算法在軟件和硬件中進(jìn)行功能劃分，從而將算法中耗時最多的Deduction模塊和Implication模塊由FPGA硬件來實現(xiàn)[10]。

該研究在硬件設(shè)計中采用了管道（Pipeline）技術(shù)，將CNF的Deduction分成了并行的N路M容量管道，并將其結(jié)果在m次周期后合并(結(jié)果)嗎，并且采用了FPGA動態(tài)加載的功能將Implication生成的learnt Clause構(gòu)成新的管道。

實驗通過DIMACS部分實例在Virtex XCV1000-6-FG680 FPGA進(jìn)行了驗證。驗證結(jié)果：沒有和其他算法進(jìn)行比較，主要對比了不同的N值下，算法速度的影響。該算法使用了FPGA中的動態(tài)配置功能，同時使用Pipeline和immerge的功能對PFGA并行能力的利用提出了新的思路。但其整體算法系統(tǒng)未完善，還未能進(jìn)行實際的實驗對比驗證，通樣存在編譯載入時間過長的問題。

（2）應(yīng)用型(Application-specified solver)算法（2002-至今）

ⅰ)應(yīng)用型SAT FPGA DP混合算法：Sousa et al.(2002)

Sousa et al.首次推出了SAT的DP應(yīng)用型FPGA硬件算法，即一次編譯下載，F(xiàn)PGA將可以解決不同的Instance問題，而不需要再編譯重載。

該算法以特殊3SAT為對象，采用寄存器陣列存儲CNF的實例將算法在軟件和硬件中分工[11-12]。如圖七所示，軟件模塊部分主要處理：沖突Conflict分析，回溯backtrack控制，語句的數(shù)據(jù)庫管理；硬件模塊部分：并行推導(dǎo)Deduction和變量選擇Decide。

通過3SAT實例在RC1000 PCI板上集成XCV2000E Xilinx FPGA和4塊SRAM(2M)的平臺上進(jìn)行了驗證。但由于沒有建立軟件接口，因而沒有進(jìn)行對比和得到實際的結(jié)果。

該研究對于應(yīng)用型的FPGA硬件算法進(jìn)行了創(chuàng)造性的嘗試，用動態(tài)更新寄存器的方法解決FPGA對于不同的實例配置的問題。采用了虛擬內(nèi)存的概念解決當(dāng)FPGA容量時的問題，但僅限于對于3SAT的解決方案。

ⅱ)應(yīng)用型SAT FPGA DP混合算法：

Skliarova et al.(2004)

Skliarova et al.采用了如圖八所示的算法，以三態(tài)存儲陣列（0，1，free）作為聯(lián)系變量和Clause陣列的矩陣模塊，從而實現(xiàn)了將SAT的實例存儲到矩陣模塊中的轉(zhuǎn)換[13]。算法為求解該矩陣每個Clause都正交向量V，如果該向量存在則SAT的實例可滿足。

實驗通過DIMACS benchmark中的幾個實例在：ADM-XRC PCI板卡上集成XCV812E V EM FPGA 40MHZ平臺上進(jìn)行了驗證。

驗證結(jié)果：和采用GRASP算法在AMD/1GHZ/256M計算機上的計算提高了2個數(shù)量級（包含實例載入的時間）

該研究采用了三態(tài)存儲陣列和矩陣模型，將應(yīng)用型SAT FPGA的算法的對象，擴展到了一般SAT實例。該算法實現(xiàn)了軟硬件的系統(tǒng)和接口，形成較完整算法功能。但提出的矩陣模型在不同應(yīng)用實例中效果和效率差異很大，并且該算法只是用硬件實現(xiàn)了SAT的算法，并未有效的利用硬件的并行處理能力。

ⅲ)應(yīng)用型SAT FPGA DP混合算法：John D.Davis et al.(2008至今)

圖五 實例型硬件算法-并行PODEM算法

圖六 實例型硬件算法-軟硬件混合算法

圖七 應(yīng)用型硬件算法1

圖八 應(yīng)用型硬件算法2

John D.Davis et al.將軟硬件模塊功能進(jìn)行較合理劃分，如圖九所示：建立和實現(xiàn)了BCP在硬件FPGA中的運算和相關(guān)接口模型[14]。算法使用了Index walk的技術(shù)更緊致的將Clause陣列存儲在BRAM中，同時采用硬件并行方式：將BCP的功能通過Inference模塊，Mulitplex合集模塊和Conflict detection模塊以及輸入輸出模塊完成。

實驗通過Crypto benchmarks和k-SAT實例（3≤k≤6）在HyperTransport(HT)和PCI-Express兩種高速板卡上集成FPGA（200MHZ）的平臺進(jìn)行的測試。

驗證結(jié)果：和采用GRASP算法在Pentium 4/3.6 GHz/2 GB RAM系統(tǒng)上的計算提高了3.7和38.6倍（包含實例載入的時間）。

該應(yīng)用型SAT FPGA DP混合算法目前為止比較完整實現(xiàn)功能的算法，其創(chuàng)造性的Index walk算法將實例有效和緊致的存儲，便于在同等資源下更大的實例計算。該算法通過多個并行的模塊對BRAM進(jìn)行操作，有效的利用了FPGA的并行性。但由于高速計算下，軟件和FPGA硬件的通訊和同步較困難，不同的實例的工作量協(xié)調(diào)成為需要解決的問題。

三、概括總結(jié)

從上面的研究情況中可以得出以下的概括總結(jié)：

（1）算法類型：分為實例型和應(yīng)用型兩種。早期的研究以實例型為主，由于對于每個實例都有漫長的編譯下載時間，其實用性和發(fā)展都有限；近期的研究都以應(yīng)用型為主，在對應(yīng)用的實例的算法加速過程中取得了初步的進(jìn)展。

（2）執(zhí)行模式：分為單純的硬件算法和混合型算法。由于FPGA硬件的資源有限，研究中大部分采用了混合型的算法，將SAT算法功能在軟件和硬件之間劃分。劃分分為兩種方式：按照計算復(fù)雜性劃分：將計算量大的，可以并行計算的功能劃分給硬件系統(tǒng)；按照存儲量或者邏輯容量來劃分，F(xiàn)PGA不能容納的部分由軟件來管理和控制。

（3）邏輯容量：硬件系統(tǒng)的計算能力受其硬件資源的限制，與應(yīng)用SAT實例需求相比始終不足，而采用了多種擴展方式進(jìn)行擴展：

?。┒鄠€硬件組成陣列的方式。

ⅱ）將硬件中的功能采用并聯(lián)或流水線的形式劃分。

ⅲ）按照硬件的存儲量和邏輯容量來劃分，其余部分軟件管理，如采用軟件系統(tǒng)中的虛擬內(nèi)存概念在硬件中調(diào)配。

（4）計算能力。硬件算法的時間由

圖九 應(yīng)用型硬件算法3

四個部分組成：硬件編譯時間，硬件配置時間，數(shù)據(jù)通訊或下載時間，實際執(zhí)行時間。實例型硬件算法受硬件編譯時間限制較大，應(yīng)用型硬件算法決定于通訊時間和實際執(zhí)行時間。但由于各種研究的硬件平臺各不相同，大都采用與類似DIMACS benchmark的實例用軟件算法的計算結(jié)果比較，但由于軟件運行的計算機系統(tǒng)的各不相同，其實際速度提升很難把握。在和軟件進(jìn)行對比中大部分采用了GRASP的SAT計算結(jié)果，但在2002年以來其計算能力就已經(jīng)被zChaff和BerkMin等越來越多的算法超越，要提高硬件算法的實用性，需要找到更有效的評估方法。

四、研究思路

實例型（Instance-Specify）的編譯配置過程本身就是一個SAT的可滿足性問題求解的過程，時間過長，在研究中將著重在更具有實用價值應(yīng)用型（application-Specify）硬件算法。硬件平臺的資源與SAT應(yīng)用的需求相比總是不足，很多SAT軟件算法中的先進(jìn)技術(shù)硬件還暫時很難實現(xiàn)，將功能在軟件和硬件上合理分工的混合型算法更具合理性。

下一步研究將致力于：1、找到合理的應(yīng)用型硬件算法，充分發(fā)揮硬件的并行處理能力，從而提高算法速度，降低同步過程中對速度的影響，達(dá)到提升整體的計算速度效果。2、建立不單純使用計算時間來進(jìn)行算法速度比較的硬件算法評估方式，使不同平臺的硬件算法速度更具有可比性和參考價值。

[1]Estrin,G.:Reconf i gurable Computer Origins:The UCLA Fixed-Plus-Variable(F+V)Structure Computer.IEEE Annals of the History of Computing.Oct.-Dec.(2002)3-9.

[2]S.A.Guccione,“Reconfigurable Computing at Xilinx,”keynote talk,EUROMICRO Symp.Digital System Design,Sept.2001.

[3]M.Davis,G.Logemann,and D.Loveland,“A Machine Program for Theorem Proving,” Comm.ACM,no.5,pp.394-397,1962.

[4]P.Goel,“An Implicit Enumeration Algorithm to Generate Tests for Combinatorial Logic Circuits,” IEEE Trans.Computers,vol.30,no.3,pp.215-222,Mar.1981.

[5]L.M.Silva and K.A.Sakallah,“GRASP: A Search Algorithm for Propositional Satisf i ability,” IEEE Trans.Computers,vol.48,no.5,pp.506-521,May 1999.

[6]B.Selman,H.Levesque,and D.Mitchell,“A New Method for Solving Hard Satisfiability Problems,” Proc.Nat’l Conf.Am.Assoc.Artif i cial Intelligence (AAAI’92),pp.440-446,July 1992.

[7]M.Yokoo,T.Suyama,and H.Sawada,“Solving Satisf i ability Problems Using Field Programmable Gate Arrays: First Results,” Proc.Second Int’l Conf.Principles and Practice of Constraint Programming,pp.497-509,1996.

[8]P.Zhong,M.Martonosi,P.Ashar,and S.Malik,“Using Configurable Computing to Accelerate Boolean Satisfiability,” IEEE Trans.Computer-Aided Design of Integrated Circuits and Systems,vol.18,no.6,pp.861-868,1999.

[9]M.Abramovici and D.Saab,“Satisfiability on Reconf i gurable Hardware,” Proc.Seventh Int’l Workshop Field-Programmable Logic and Applications,pp.448-456,1997.

[10]A.Dandalis and V.K.Prasanna,“Run-Time Performance Optimization of an FPGA-Based Deduction Engine for SAT Solvers,” ACM Trans.Design Automation of Electronic Systems,vol.7,no.4,pp.547-562,Oct.2002.

[11]J.de Sousa,J.P.Marques-Silva,and M.Abramovici,“A Conf i gware/Software Approach to SAT Solving,” Proc.Ninth IEEE Int’l Symp. Field-Programmable Custom Computing Machines,2001.

[12]N.A.Reis and J.T.de Sousa,“On Implementing a Configware/Software SAT Solver,” Proc.10th IEEE Int’l Symp.Field-Programmable Custom Computing Machines,pp.282-283,2002.

[13]I.Skliarova and A.B.Ferrari,“A Software/Reconf i gurable Hardware SAT Solver,” IEEE Trans.Very Large Scale Integration (VLSI) Systems,vol.12,no.4,pp.408-419,Apr.2004.

[14]Kestur,S.; Davis,J.D.; Williams,O .“BLAS Comparison on FPGA,CPU and GPU” VLSI (ISVLSI),2010 IEEE Computer Society Annual Symposium 2010.

[15]DIMACS challenge benchmarks.[Online].Available:http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/benchm.html.