基于不完全算法的并行FPGA SAT求解器*

黎鐵軍，馬柯帆，張建民

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

1 引言

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

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

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

2 研究現(xiàn)狀

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

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

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

3 并行FPGA SAT求解算法

SAT求解的流程如圖 1所示。預(yù)處理器使用純文字規(guī)則對(duì)SAT實(shí)例進(jìn)行化簡(jiǎn)，這個(gè)過程不會(huì)改變實(shí)例的可滿足性[8]。此外，預(yù)處理還產(chǎn)生多組當(dāng)前賦值不滿足的子句、變?cè)跏假x值。

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

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

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

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

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

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

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

并行FPGA SAT求解器的主要目的是使用當(dāng)前先進(jìn)的硬件平臺(tái)，以更高效、便捷的方式求解超大規(guī)模的SAT實(shí)例。由于實(shí)例提取的子句信息、變?cè)x值等均存儲(chǔ)在FPGA的片上RAM，因此隨著實(shí)例規(guī)模的增大，求解器消耗的邏輯資源會(huì)急速增長。對(duì)XILINX Virtex-6 FPGA (XC6VHX565T)芯片，在單線程的情況下片上RAM的使用率可達(dá)到95%。對(duì)pprobSAT+并行求解器，勢(shì)必需要更大規(guī)模的FPGA才能實(shí)現(xiàn)，考慮到實(shí)驗(yàn)的首要目的是驗(yàn)證求解器的可行性和可擴(kuò)展性，以下實(shí)驗(yàn)來源于功能仿真結(jié)果。實(shí)驗(yàn)中預(yù)處理部分均在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進(jìn)行仿真實(shí)驗(yàn)。

由于pprobSAT+求解器是一個(gè)基于不完全算法求解器，因此選取的測(cè)試用例是可滿足的實(shí)例，為了便于功能仿真過程中實(shí)驗(yàn)結(jié)果的觀察與分析，本文選取SATLIB Benchmark Problems小規(guī)模的隨機(jī)實(shí)例uf50-01測(cè)試。問題規(guī)模為50個(gè)變?cè)?18個(gè)子句。雖然實(shí)例規(guī)模較小，但從問題求解的難度來說，實(shí)例子句變?cè)染幱谂R界值4.26左右，其不可滿足和可滿足的概率幾乎是相等的，屬于難解的一類問題集。

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

Table 1 Performance comparison表1 性能對(duì)比

5 結(jié)束語

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