黎鐵軍，馬柯帆，張建民

(國防科技大學計算機學院，湖南 長沙 410073)

1 引言

可滿足性問題SAT(SATisfiability problem)作為最著名的NP完全NPC(Non-deterministic Polynomial Complete)問題之一，被廣泛應用于理論研究和實踐領域。許多困難的組合問題，包括硬件與軟件的形式化驗證、人工智能、運籌學、計算生物學、密碼學、數(shù)據(jù)挖掘和機器學習等方向出現(xiàn)的問題，都可以用基于SAT的技術(shù)來解決。自從關于在可重構(gòu)硬件上實現(xiàn)SAT求解器的綜述[1]發(fā)表以來，基于硬件的SAT求解器獲得了飛速的發(fā)展。最壞情況下，SAT問題求解時間呈指數(shù)增加，因此，近年來針對如何利用FPGA固有的靈活性和并行性高效求解SAT問題成為業(yè)界研究的熱點。

SAT問題求解的最終目的是獲得高效正確的判定。SAT求解器在不斷追求高效算法的同時，不可避免地會遇到一些問題[2]。對軟件求解器來說，一些求解器盡管性能優(yōu)異，但求解算法過于復雜，研究人員需要大量專業(yè)知識去理解概念的正確性和算法運行機制。一些已經(jīng)解決的問題或許還存在更優(yōu)的求解方法。此外，一些求解器一味地追求其性能而忽視了算法的完備性，甚至正確性。對硬件求解器來說，軟件求解器中新的啟發(fā)式和數(shù)據(jù)結(jié)構(gòu)的應用對硬件SAT求解器的加速策略作出了顯著貢獻。然而，尚不清楚硬件SAT求解方案的總體進展是否跟上了日益復雜和高效的軟件求解器的快速進步?；谟布腟AT求解器仍面臨諸多挑戰(zhàn)[3]。

本文重點研究了基于隨機局部搜索SAT求解器的算法與實現(xiàn)，提出了基于FPGA的并行多線程求解器pprobSAT+。但是，與以往單線程求解器不同的是，pprobSAT+是線程級的硬件并行求解器，由于使用多線程執(zhí)行的策略，避免了搜索過程中的等待延時，提高了求解效率。實驗結(jié)果表明，相比于單線程求解器，本文提出的三線程并行求解器的求解效率有顯著提高，最大可達2.4倍的加速。

2 研究現(xiàn)狀

求解SAT問題有許多不同的算法，這些算法基本上可以分為2類：完全算法和不完全算法。完全算法總是可以找到使公式滿足的解或者推斷出問題不可滿足。其優(yōu)點是能準確判定SAT問題是否滿足，當實例無解時可以給出完整的證明，但其缺點是解空間的復雜度會隨著問題規(guī)模的不斷增大呈指數(shù)增長，因此，早期的完全算法僅僅適合求解小規(guī)模的SAT問題，且計算效率不高。

不完全算法主要是基于局部搜索算法[4]和遺傳算法[5]。文獻[6,7]分別提出了一種基于加強約束和概率分布函數(shù)的FPGA SAT求解器。通常，不完全算法不能保證在指定的步驟內(nèi)找到問題的解。當解存在時，意味著SAT問題可滿足，反之，不能說明該問題不可滿足。

近年來，完全算法在解決布爾可滿足性等許多現(xiàn)實問題方面取得了很大的進展，但由于搜索空間的急劇增大，它們往往不能很好地擴展。解決組合爆炸問題的一種方法是犧牲完備性，使用這種策略的最著名的方法是局部搜索算法。通常，局部搜索策略從初始賦值開始，該初始賦值可以是隨機生成的，也可以是啟發(fā)式生成的。然后，根據(jù)目標函數(shù)將搜索總是轉(zhuǎn)移到較好的鄰域，如果目標達到或找不到更好的解，則終止搜索。與完全算法相比，不完全算法一般速度更快，單位時間迭代次數(shù)更多。對于某些類型的SAT問題，如3-SAT，特別是較大規(guī)模的3-SAT，其效率更高。

3 并行FPGA SAT求解算法

SAT求解的流程如圖 1所示。預處理器使用純文字規(guī)則對SAT實例進行化簡，這個過程不會改變實例的可滿足性[8]。此外，預處理還產(chǎn)生多組當前賦值不滿足的子句、變元初始賦值。

Figure 1 Flow chart of SAT solving system圖1 SAT求解的流程圖

對軟件求解器來說，并行求解算法主要是使用不同的種子和參數(shù)在不同的 CPU 核上執(zhí)行多個任務，以達到并行求解的目的。本文提出的基于不完全算法的并行多線程求解器就是基于這個概念，它是文獻[7]提出的基于概率分布的單線程FPGA SAT求解器在實現(xiàn)方式上的進一步延伸。本文提出的基于不完全算法的并行多線程求解器的基本思想是，對相同的SAT實例，主機提取的地址映射表以及子句映射表是一致的?；趐probSAT+的并行硬件求解器，最直觀的處理方式是在同一塊或者多塊FPGA中復制多個完整的求解器。在算法求解過程中，這些求解器使用不同的策略(如不同的初值、隨機數(shù)生成器產(chǎn)生的不同地址)對同一實例進行并行求解，任何一個求解器找到問題的解即搜索停止，問題可滿足。反之，只有在規(guī)定的時間或者步數(shù)內(nèi)所有求解器均不能找到解，搜索才能停止。然而正如文獻[2]所描述的，算法在搜索的過程中，要最終確定當前賦值不滿足的子句中實際翻轉(zhuǎn)的變元，需要臨時翻轉(zhuǎn)子句寄存器中的3個文字，評估各文字相關的子句并計算對應的break-value值。由于算法是順序執(zhí)行，因此在搜索的不同階段，勢必會使電路中的某些部件處在空閑狀態(tài)。若采用簡單的復制多個求解器的方式必然會帶來很大的資源浪費，特別是導致片上存儲器的大量浪費。利用多線程策略，對相同的實例嘗試更改初始賦值，以實現(xiàn)MAX-TRIES搜索，不同線程均對同一地址和子句映射表進行數(shù)據(jù)交互，則會大幅度地減少片上存儲器的資源開銷，并且由于使用多線程策略，每秒總翻轉(zhuǎn)量將會成倍地增加，有更大的概率在規(guī)定的時間內(nèi)找到問題的解(如果存在的話)。多線程求解示意圖如圖2所示。

Figure 2 Multi-thread solving圖2 多線程求解框圖

Figure 3 pprobSAT+ achitecture圖3 pprobSAT+求解器結(jié)構(gòu)

求解器硬件結(jié)構(gòu)如圖3所示。在pprobSAT+并行求解器中，搜索開始前，主機根據(jù)實例提取相關數(shù)據(jù)：(1)給定問題的子句數(shù)據(jù)，(2)對變元的多組初始賦值，圖3中Nv表示變元數(shù)量；(3)對應賦值下的不可滿足的子句信息，并將數(shù)據(jù)下載到電路中。其中，多組初始賦值和不可滿足子句是用于多線程搜索的。子句數(shù)據(jù)存儲在地址和子句映射表中，不同的初始賦值存儲于子句評估模塊中的變元表中(每個變元表存儲一組初始賦值)。對于XILINX Virtex-6 FPGA (XC6VHX565T)芯片，其內(nèi)部包含多達912個片上RAM(容量為36 Kb)，每個RAM可以拆分成2個獨立的18 Kb RAM塊使用,因此在未使用片外存儲器的情況下最多可求解36 Kb的變元，若要求解更大規(guī)模的實例則需要多個RAM塊。多組當前賦值下不可滿足的子句存儲在不同的不可滿足子句存儲器中。同樣地，pprobSAT+求解器主要用于求解3-SAT問題。

在pprobSAT+并行求解器中，選擇緩存器存儲的當前賦值下不可滿足的子句是隨機的。電路中不可滿足子句寄存器的大小為4 096。假設不可滿足子句寄存器中的子句數(shù)為m,此時，需要在0到m中生成一個隨機數(shù)來作為地址選擇寄存器中當前賦值下的不可滿足子句。隨機數(shù)產(chǎn)生模塊由D觸發(fā)器和若干個異或門組成的線性反饋移位寄存器來實現(xiàn)，產(chǎn)生一個21 bit的隨機數(shù)NR，為了避免搜索過程中的除法運算，預先計算出1/m(m=1，…，4 095)的值，并將值左移20位的結(jié)果存儲在片上RAM中。最終不可滿足子句寄存器中的地址r由NR對m取模得出。

4 實驗結(jié)果與分析

并行FPGA SAT求解器的主要目的是使用當前先進的硬件平臺，以更高效、便捷的方式求解超大規(guī)模的SAT實例。由于實例提取的子句信息、變元賦值等均存儲在FPGA的片上RAM，因此隨著實例規(guī)模的增大，求解器消耗的邏輯資源會急速增長。對XILINX Virtex-6 FPGA (XC6VHX565T)芯片，在單線程的情況下片上RAM的使用率可達到95%。對pprobSAT+并行求解器，勢必需要更大規(guī)模的FPGA才能實現(xiàn)，考慮到實驗的首要目的是驗證求解器的可行性和可擴展性，以下實驗來源于功能仿真結(jié)果。實驗中預處理部分均在Intel(R)Core(TM)i5-6400 64-bit 2.7 GHz CPU 8.0 GB RAM和Linux Ubuntu-14.04環(huán)境下編譯和執(zhí)行。求解器使用Verilog硬件描述語言，在ISE 14.7環(huán)境下開發(fā)，并使用Mentor Graphics公司的Modelsim SE-64 10.4進行仿真實驗。

由于pprobSAT+求解器是一個基于不完全算法求解器，因此選取的測試用例是可滿足的實例，為了便于功能仿真過程中實驗結(jié)果的觀察與分析，本文選取SATLIB Benchmark Problems小規(guī)模的隨機實例uf50-01測試。問題規(guī)模為50個變元、218個子句。雖然實例規(guī)模較小，但從問題求解的難度來說，實例子句變元比均處于臨界值4.26左右，其不可滿足和可滿足的概率幾乎是相等的，屬于難解的一類問題集。

本文從 2011 年 SAT 競賽的測試基準庫[9]中選取 4個小型和2個中型的隨機實例進行驗證。三線程并行求解器pprobSAT+相對單線程求解器 probSAT+[6]的性能增益如表1所示。probSAT+求解器系統(tǒng)結(jié)構(gòu)與預處理方式類似于pprobSAT+，區(qū)別在于前者為單線程求解。表1中是軟件仿真結(jié)果，考慮到對隨機產(chǎn)生的地址來說，并不能做到完全隨機，最終的地址由偽隨機數(shù)產(chǎn)生，也就是說在使用的種子不變的情況下，每次產(chǎn)生的隨機數(shù)是確定的，為了更公平地比較求解效率，測試中對每個實例獨立運行 5 次，所得的數(shù)據(jù)為 5次測試的平均值。不難發(fā)現(xiàn)，當實例規(guī)模很小時，產(chǎn)生的當前賦值下不可滿足的子句數(shù)相對較少，多線程并行求解器并不能獲得很高的加速比，隨著實例規(guī)模的不斷增大，相比單線程求解器，多線程并行求解器可獲得超過2倍的加速比。

Table 1 Performance comparison表1 性能對比

5 結(jié)束語

本文提出了一種在 FPGA 上實現(xiàn)并行多線程 SAT 求解器的新方法pprobSAT+。在求解的過程中，3個獨立的線程被同時執(zhí)行，以使并行和流水線電路具有很高的求解性能。當實例規(guī)模滿足所有的數(shù)據(jù)都存儲在 FPGA 片上存儲器時，本文提出的求解器pprobSAT+能獲得最大性能。若能將部分數(shù)據(jù)存于片外存儲器，則能大大提高求解器處理問題的規(guī)模。本文僅對提出的并行多線程求解器進行了初步的功能仿真，求解器時序仿真以及布局布線方面的優(yōu)化還需要進一步分析。除此之外，該求解器的另一個局限性是當前的最大值設置為30，若要求解具有更大規(guī)模的SAT問題，需要進一步研究流水線的執(zhí)行方式。為了達到這些目的，需要對電路進行改進，使其能夠動態(tài)地改變流水線的長度，這也是未來研究的方向之一。