基于硬件可編程邏輯（FPGA）的SAT算法的綜述

中山大學邏輯與認知研究所 周 進 趙希順

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

可編程硬件算法研究的發展是和硬件水平的發展密不可分的。可編程硬件是指最早的硬件可編程算法的概念是G.Estrin在1960年左右提出的[1]，但由于主要以分立器件為硬件平臺，而集成電路也尚在初期，因此并未得到更多研究和應用的支持。從1990年開始，超過10K門級的可編程邏輯器件FPGA（其典型結構如圖一所示）的出現，使得硬件可編程邏輯算法的研究進入了蓬勃發展的時期[2]，其應用主要分為三種：1、硬件設計模擬；2、快速硬件成樣；3、硬件算法研究。而其中硬件算法研究是基于FPGA硬件并行處理能力，已經在密碼學，圖像和信號處理領域取得了很多成果。自1997年后，隨著FPGA進入到了百萬門級的水平，硬件可編程邏輯能力上升到了一個新的高度，基于硬件可編程邏輯的高難度算法的實現與研究也受到越來愈多的關注。其中，基于FPGA的可滿足性問題（SAT問題）的算法研究逐漸成為研究的熱點[7-14]。

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

一、問題定義

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

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

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

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

二、研究進展現狀和發展趨勢

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

● 實例型（Instance-Specified Solver）算法：硬件結構針對每一個實例進行編譯配置然后計算的方式，每一個不同的實例對應不同的硬件結構。

● 應用型（Application-specified solver）算法：硬件結構針對應用進行一次編譯和配置然后計算，在同一個硬件機構上對應用中不同的實例進行計算。

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

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

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

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

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

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

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

圖一 FPGA 的典型結構

圖二 DP算法舉例

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

圖四 實例型硬件算法-有限狀態機

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

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

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

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

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

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

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

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

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

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

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

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

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

該研究對于應用型的FPGA硬件算法進行了創造性的嘗試，用動態更新寄存器的方法解決FPGA對于不同的實例配置的問題。采用了虛擬內存的概念解決當FPGA容量時的問題，但僅限于對于3SAT的解決方案。

ⅱ)應用型SAT FPGA DP混合算法：

Skliarova et al.(2004)

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

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

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

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

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

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

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

圖七 應用型硬件算法1

圖八 應用型硬件算法2

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

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

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

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

三、概括總結

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

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

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

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

ⅰ）多個硬件組成陣列的方式。

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

ⅲ）按照硬件的存儲量和邏輯容量來劃分，其余部分軟件管理，如采用軟件系統中的虛擬內存概念在硬件中調配。

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

圖九 應用型硬件算法3

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

四、研究思路

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

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

[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.