基于改進連續時間動態系統的模擬SAT求解器

趙海軍 陳華月 崔夢天

摘 要：針對布爾可滿足性問題的高效求解進行了研究。首先，通過對k-SAT問題和基于耦合常微分方程形式的確定性連續時間動態系統的分析，提出了一種基于時延信息形式的改進連續時間動態系統方程，以保持集中搜索特性；然后，提出了實現該系統方程的三個主要組件即信號動態電路、輔助變量電路和數字驗證電路的模擬設計。在信號動態電路的設計中，設計了一種獲得更高性能、更小面積和更低功耗的模擬硬件形式；在提出的輔助變量電路和數字驗證電路的模擬硬件設計中，實現了避免梯度下降搜索陷入無解和確定給定問題的解是否已經找到的目標；同時提出了降低面積和功耗的可替代輔助變量電路的兩種設計方案。仿真實驗結果表明，提出的新的模擬SAT求解器不僅是有效的，而且相比于單一軟件算法實現的SAT求解器和其他硬件類SAT求解器具有更高的加速性能和更低的功耗。

關鍵詞：布爾可滿足性問題；連續時間動態系統；模擬設計；輔助變量；數字驗證；加速性能

中圖分類號：TP331?? 文獻標志碼：A?? 文章編號：1001-3695（2024）01-030-0200-06

doi：10.19734/j.issn.1001-3695.2023.04.0189

Analog SAT solver based on improved continuous-time dynamic systems

Abstract：This paper studied efficient solving of the Boolean satisfiability problem.Firstly，by analyzing the k-SAT problem and the deterministic continuous-time dynamical system based on the coupled ordinary differential equation form，this paper proposed an improved continuous-time dynamical system equation based on the time-delay information form to maintain the centralized search property.Then，it presented the analog design of three main components，namely，the signal dynamics circuit，the auxiliary variable circuit and the digital verification circuit，to implement the system equation.In the design of signal dynamics circuit，this paper designed a form of analog hardware to obtain higher performance，smaller area and lower power consumption.In the analog hardware design of the proposed auxiliary variable circuit and digital verification circuit，it achieved the goal of avoiding the gradient descent search falling into no solution and determining whether the solution of a given problem has been found.At the same time，it proposed two design schemes of alternative auxiliary variable circuit with reduced area and power consumption.The simulation results show that the proposed new analog hardware SAT solver is not only effective，but also has higher speedup performance and lower power consumption compared with the SAT solver implemented by only software algorithm and other hardware SAT solvers.

Key words：Boolean satisfiability problem；continuous-time dynamical system；analog design；auxiliary variables；digital verification；speedup performance

0 引言

隨著摩爾定律的過時，探索新的計算范式顯得比以往任何時候都更有必要。盡管量子計算是一個很有前途的領域，但在物理學和工程方面仍面臨許多挑戰。神經形態計算如細胞神經網絡（cellular neural network，CNN）［1，2］已被證明是解決感官處理（視覺和模式識別）和機器人技術等一系列問題的有效替代方案。模擬混合信號信息處理系統（如CNN）可以為一些通過數字計算機解決的困難問題提供極具功率/能量高效的解決方案，這類系統近年來受到越來越多的關注［3-5］。在模擬計算系統中，算法（代表軟件）是一個動態系統，通常在實數上以連續時間運行的微分方程形式來表達，其物理實現（硬件）是任意的物理系統如模擬電路，其行為由相應的動態系統來描述。設計動態系統的方程，使問題的解作為動態性的吸引子出現，計算的輸出是這些吸引子的收斂狀態的集合。盡管已經表明常微分方程系統可以模擬任意計算機［6］，但它們還沒有得到廣泛普及，因為設計這樣的系統是針對于特定問題的，即通常是困難的。然而，如果可以設計一種有效的模擬機制來求解NP-完全問題，將有助于高效求解NP類中的所有問題［7］。本文研究設計模擬硬件來解決具有代表性的NP-完全問題，即布爾可滿足性（satisfiability，SAT）問題。SAT是許多電子設計自動化問題的關鍵，也是許多決策、調度、差錯糾正和安全應用的核心。眾所周知，對于k≥3的k-SAT問題來說，它是NP-完全的［7］。

目前常用的確定性序列離散軟件算法利用搜索空間的某些特性［8］，其他算法基于啟發式，盡管它們可能在某些SAT公式上表現較好，但需要耗費指數級長的時間。如文獻［9］提出的基于SAT的故障樹分析方法、文獻［10］提出的決定3-SAT的可滿足性的多項式時間（和空間）算法、文獻［11］提出的基于SAT求解器的組合電路重匯聚現象分析法和文獻［12］提出的基于擴展規則的布爾可滿足性貪婪局部搜索算法等SAT求解器，通常包括判決、演繹、沖突分析和其他功能，利用數字計算機的能力為文字賦值、進行布爾約束傳播（Boolean constraint propagation，BCP）和回溯沖突。也有學者提出了一些基于硬件的SAT求解器。如文獻［13，14］提出了基于FPGA的解決方案用于現代SAT求解器中得到BCP部分，這些基于FPGA的求解器與單一的高性能軟件求解器［10］相比，加速性能有所提高；文獻［15］提出了一種基于專用數字集成電路（integrated circuit，IC）的SAT求解器，實現了通用任務分配軟件模式的一種變體，可加速隱含圖的遍歷和沖突子句的生成，這些基于硬件的方法性能仍有很大的改進空間，因為這些硬件加速器所基于的算法是基于數字計算機設計的，通常只能實現有限的加速。相比之下，本文方法用時間成本換取能量成本，這在實際應用中比大量硬件資源更可取。

從工程的角度來看，理想的方法需要結合兩類權衡：時間與能量，以及時間與硬件。對此，本文提出了一種新的模擬硬件（analog hardware，AH）SAT求解器，稱之為AH-SAT求解器。提出的模擬方法是完全確定的，并提取了關于解的最大信息，隱含地嵌入到子句系統中，可以高效地求解困難的基本SAT問題。具體來說，AH-SAT基于耦合常微分方程形式的確定性連續時間動態系統（continuous-time dynamical system，CTDS）；基于SPICE的仿真結果表明，提出的AH-SAT相比于軟件實現的SAT求解器，平均實現了超過104倍的加速，相比于其他硬件類實現，在加速和功耗方面的性能也大大提高。

1 k-SAT問題及改進的連續時間動態系統

容易看出，當且僅當Km=0時，子句Cm是滿足的。定義一個“勢能”函數為

其中：am＞0為輔助變量。當且僅當V=0時，所有子句都是滿足的，因此，SAT問題可以重新表述為在s中搜索V的全局極小值。如果輔助變量am保持為常數，那么對于大多數困難問題，任何下降確定性算法將最終陷入V的局部極小值而無法找到解。為了避免這種情況，將輔助變量賦予與模擬子句函數Km耦合的時間依賴性：

式（3）描述了V的梯度下降，式（4）是一個由Km的不滿足程度驅動的指數增長（保證在任何時候am（t）＞0）。式（3）可以改寫為

對于輔助變量am，式（4）的形式解為

因此，V的表達式（式（2））是由動態過程中最久未被滿足的那些Km項所控制。注意，連續時間動態系統式（3）（4）不是唯一的，但從理論角度來看，它是簡單的，由于輔助變量的指數加速，它包含了求解任意SAT問題的必要因素。

可以看到，盡管尋找解的模擬時間t的規模是多項式，但在硬件實現中，am變量代表電壓或電流，因此尋找解所需的能量資源對于困難公式來說可能變成指數級的。然而，am變量無須像式（4）那樣無限地呈指數增長，因此式（4）并不適合物理實現。要尋找其他變體，這些變體要明顯優于純數字算法，但在物理實現和成本方面又是可行的，因此本文提出將時間成本轉換為能量成本。為此，引入另一種基于時延信息的形式，它既保持了集中搜索特性，但當相應子句（接近）滿足時，又允許am減小，m：

要求： am（0）>0，δm（0）=0（9）

其中：延遲函數δm（t）∈［0，t］確定影響am變化的Km（s（t））軌跡的歷史窗口。式（8）的解形式為

顯然，δm（t）=t對應于式（4），δm（t）=0為恒定am即am（0）的情形，它對應于實際能量最小化的情形。一種選擇δm（t）的方法就是最初將其設置為一個較小值，并在每次動態停滯或達到一個較高的閾值時將其加倍（如設置為允許的最大電壓值），這通常只需要若干次迭代。由于這種時延形式導致滿足子句的關聯am的減小，相對降低了式（5）中子句的權重，從而增加了集中搜索空間中其他子句的權重，增強了不滿足子句的驅動能力。下面提出實現上述系統方程的模擬硬件設計。

2 系統方程的模擬硬件設計

圖1描述了本文提出的AH-SAT的層次架構，它由三個主要組件構成：信號動態電路（signal dynamics circuit，SDC）、輔助變量電路（auxiliary variable circuit，AVC）和數字驗證電路（digital verification circuit，DVC）。AVC包含M個元件，對應M個子句，每個元件從SDC接收相關si的信號作為輸入，并生成am（m∈［1，M］）個變量作為輸出。SDC包含N個元件，對應N個變量，依次從AVC接收am作為反饋，并相應地演變si（i∈［1，N］）信號。SDC輸出si的模擬值到AVC，輸出si的數字形式到DVC。基于si的數字值，DVC確定給定SAT問題的解當時是否已經找到。提出的架構可以求解任意具有N個布爾變量和M個子句的k-SAT問題，下面以3-SAT問題（即對于每個子句j有三個非零cm，j）為例詳細說明三個電路組件的設計。對于任意k-SAT問題來說，AH-SAT都可以遵循這個原則來設計。

2.1 信號動態電路

SDC包含一組模擬元件，實現式（5）（6）的動態性，目標是設計一種模擬硬件形式來獲得更高的性能、更小的面積和更低的功耗。事實上，本文設計的精確性對于所考慮的動態系統類型是足夠的。給定一個有N個變量的3-SAT問題，SDC包含

為了說明圖2（a）中的si元件可以用來計算式（5），將來自每個分支塊的電流表示為Im，i，則有

由式（12）可以看出，Dm，i具有以下性質：

a）如果si、si2和si3中的任意一個滿足，即達到1或-1（表明xi為true或false），則Dm，i為零，根據式（5），Dm，i為零表示子句Cm對si的變化沒有影響。另一方面，當三個變量一個都不滿足但其中一個更接近滿足時，Dm，i的量值減小。

b）Dm，i的符號與cm，i的符號相同，因為（1-si）不能為負。如果cm，i=1（或-1），則Dm，i對dsi/dt的貢獻為正（或為負），即它嘗試將si推向+1（或-1）。

注意，盡管式（14）中的Vam（作為兩個NAND門的輸入）好像被看成一個數字信號，但當NAND門和反相器在線性Vin～Vout工作時，它實際上仍然是一個模擬信號，以產生所需的模擬輸出。

SDC還通過反相施密特觸發器將模擬信號Vi轉換為數字信號Qsi，反相施密特觸發電路如圖4（a）所示。然后，數字信號發送到DVC，以檢查是否找到了解。從圖4（b）的仿真結果可以看出，反相施密特觸發電路的傳遞曲線存在遲滯現象，因此它可以在噪聲影響最小的情況下進行模/數轉換。綜合以上討論可見，SDC正確地實現了式（3）所定義的系統動態性。

2.2 輔助變量電路和數字驗證電路

式（4）中定義的輔助變量am用來幫助避免梯度下降搜索陷入無解。在子句Cm的不滿足程度的驅動下，am信號遵循指數增長。實現指數函數的一種直接方法是通過一個運算放大器（operational amplifier，OA）。

AVC包含一組M個am元件，M是給定問題中的子句數。圖5所示為類似于非反相積分器的am元件的原理設計。這里，am的值（對于子句Cm）用運放的輸出端電壓Vam來表示，電阻元件Ri1、Ri2、Ri3分別與R′i1、R′i2、R′i3一樣，兩個電容C和C′值也相同。由EN控制的開關通過一個傳輸門實現，控制am元件的啟動。Vam的一階微分方程可以寫為

圖5中的R是由傳輸門實現的可調電阻元件，類似于圖3中的綠色框所示。例如，對于Ri1和R′i1，傳輸門（Mp和Mn）通過其他四個傳輸門，由模擬信號Vi1和V′i1控制，表示xi出現在子句Cm中。另外兩對R的設計方法是一樣的。如果子句Cm中的三個變量中的任何一個滿足，相應的Vi就關閉各自的傳輸門，并切斷運放的反相輸入到GND和非反相輸入到Vam的電流路徑。

盡管圖5給出的AVC設計實現了指數級增長，但它需要M個運放，從而導致大面積和大功耗。本文將在2.3節提出可替代的AVC設計。DVC的目標是確定給定問題的解（si的集合）是否已經找到。通過利用如圖6所示的3M個異或（XOR）門陣列和M個與非（NAND）門陣列，很容易實現DVC。DVC的輸入是si和-si的數字表示Qsi和si，來自于SDC。每個NAND門對應一個子句，其輸入對應子句中出現的文字。注意，在DVC中，只包括那些值為+1（由邏輯信號“1”表示）和-1（由邏輯信號“0”表示）的cm，i。可見，SDC、AVC和DVC這三個組件都是模塊化的和可編程的。通過模塊化，每個電路中的基本元件可以針對不同的問題規模（即變量數目N和子句數目M）重復；通過可編程，任何k-SAT問題實例都可以通過相同的SDC、AVC和DVC實現，只要問題規模小于或等于硬件規格。

2.3 可替代的AVC設計

2.2節中提出的基于運放的AVC實現了指數級增長的am變量，目的是解決在其物理限制內的困難SAT問題（如具有約束密度α=M/N≥4.25的一些SAT實例）。然而，對于應用類SAT問題，即不是特別難的問題，am的指數級增長并不總是必要的。下面提出兩種替代電路設計，以實現具有（1-ε2e-qt）型增長到飽和值的am功能。以下將這個形式的am 增長稱為“更簡單的形式”。圖7所示為實現更簡單am增長的am元件的原理設計，其中電容C通過三個可調電阻充電到VDD。控制Vam的一階微分方程可以寫成

注意，由于圖7的電路無法實現式（4）的指數級增長，即使對于許多困難問題，在尋找較小規模問題的解（只要是可求解的）時，它比基于運放的am元件更有效。后面評價部分的仿真結果將表明這一點。

3 方案評價

為了對本文所提出的模擬硬件SAT求解器AH-SAT的性能進行評價，仿真實驗所采用的硬件配置為：CPU采用雙核Intel Core 2 Duo 3.0 GHz處理器，GPU采用NVIDIA GeForce RTX 3060，內存大小為64 GB。仿真環境采用基于32 nm CMOS工藝的電路仿真軟件HSPICE在晶體管級構建所有功能電路，并應用C++輔助編程；所有功能電路元件電源電壓設置為VDD=1 V。為獲得足夠的驅動能力，仿真中將最小晶體管尺寸設置為W=1 μm，L=40 nm。對于邏輯門，晶體管尺寸選擇以確保相等的上拉和下拉強度。對于圖3中的分支塊，晶體管Mp1和Mn1的W/L值（即Ra的大小）關于其他晶體管的W/L值（即Ri、Ri2和Ri3的大小）決定了am對Im，i的貢獻，因此，要考慮Ra的大小am的影響之間的權衡，在實現中，選擇晶體管尺寸使得Ra與Ri、Ri2和Ri3的比值分別為64、4和4。其他電路中晶體管的尺寸也以類似的方式確定。

仿真過程首先運行命題公式 F，確定3-SAT問題是NP-完全問題。其中F表示公式，C表示字句，采用以下歸結算法來實現。

算法1 歸結算法

function resolution（F）

F′=；

repeat

F←F∪F′；

for all Ci，Cj∈F do

C′=resolve（Ci，Cj）；

if C′=⊥ then

return unsat；

end if

F′←F′∪{C′}；

end for

until F′F

return sat；

end function

為了表明AH-SAT具有式（3）和（4）的CTDS動態性，實驗測試信號si和am的波形。圖9為對于一個有50個變量和212個子句的3-SAT問題實例測得的三組si和am波形，問題/公式的約束密度α=M/N=4.25（困難問題）。圖9中，（a）為基于運放的am實現，實現ε1eqt型am增長；（b）為更簡單的am實現，實現1-ε2e-qt型am增長；（c）為延時更簡單的am實現；可以看到，對于三種設計，AH-SAT在一定時間后都成功地找到了解，即垂直虛線所示。從si軌跡可以看出，在找到解后，si信號趨于穩定（即收斂）。比較三種不同設計中的am軌跡可以看到，在基于運放的設計中，由于指數級增長函數，am的增長最快，而在延時實現中，一些am（對應于滿足的子句）在達到其峰值后下降，正如式（8）所預測的那樣。

這些結果表明，在相同的物理約束條件下，基于am指數增長的AH-SAT能夠更好地處理較大規模的問題，而具有1-ε2e-qt型am增長的AH-SAT能夠更有效地處理較小規模的問題。

為了進一步表明AH-SAT的有效性，將基于更簡單的am的AH-SAT設計與采用自適應龍格-庫塔-Cash-Karp（Runge-Kutta&Cash-Karp，RK&CK）方法（5階）求解系統式（3）（4）的軟件實現和文獻［10］的軟件求解器進行比較。兩種軟件實現在相同的計算機上運行，隨機生成5 000個困難的（α=4.25）3-SAT問題，每個問題的大小為N=10、20、30、40和50，包含1 000個實例，應用相同的初始條件。表1為對于每個問題規模找到解所需的平均時間。其中AH-SAT列給出AH-SAT所花費的模擬/物理時間，RK&CK和MiniSat列分別給出了兩種軟件實現的CPU運行時間。可以看到，RK&CK列的時間隨問題規模的增加幾乎呈指數級增加，這是很自然的，因為數值積分是在計算機上進行，為了確保計算軌跡的預先設定精度，RK&CK算法必須進行大量的窗口精細離散化步驟；從表1的數據還可以看出，AH-SAT相比于軟件實現的RK&CK和MiniSat，平均加速因子分別提高了105～106倍和約104倍。

表2所示為AH-SAT與目前先進的基于硬件的兩種方法的加速性能和功耗性能比較。從表2可以看到，AH-SAT也非常具有競爭力。例如，與文獻［14］的基于CPU+FPGA的求解器和文獻［15］的專用數字IC實現相比，對于相同規模的問題，AH-SAT在平均加速性能和平均功耗性能方面分別提高了大約104倍和4倍以及103倍和3.5倍。AH-SAT的功耗主要是由于模擬反相器和NAND門的靜態功耗引起的。

4 結束語

本文提出了一種基于CTDS的原理驗證模擬硬件系統AH-SAT來求解3-SAT問題，該設計可以很容易地擴展到一般的SAT問題，提出的AH-SAT是模塊化的和可編程的，可以用作SAT求解協處理器。提出了三種不同的設計方案來實現由CTDS所要求的輔助變量動態性，基于SPICE的仿真結果表明，提出的AH-SAT相比于軟件實現的SAT求解器，平均實現了超過104倍的加速，相比于其他硬件類實現，在加速和功耗方面的性能也大大提高。這表明本文設計的模擬硬件SAT求解器作為離散優化處理器具有很大潛力。對于未來的工作，將研究輔助變量動態性的可替代實現，以及處理不適合于給定硬件實現的問題實例的方法。與模擬硬件相關的特有挑戰如噪聲和制作工藝變化也將是進一步研究的方向。

參考文獻：

［1］蔣東華，劉立東，王興元，等.基于細胞神經網絡和并行壓縮感知的圖像加密算法［J］.圖學學報，2021，42（6）：891-898.（Jiang Donghua，Liu Lidong，Wang Xingyuan，et al.Image encryption algorithm based on cellular neural network and parallel compressed sen-sing［J］.Journal of Graphics，2021，42（6）：891-898.）

［2］張小紅，廖琳玉，鐘小勇.一種憶阻細胞神經網絡的電路設計方法：中國，CN104573238B［P］.2018-11-19.（Zhang Xiaohong，Liao Linyu，Zhong Xiaoyong.A circuit design method for memristor cell neural networks：China，CN104573238B［P］.2018-11-19.）

［3］Husain S，Imran M，Ahmad A，et al.A study of cellular neural networks with vertex-edge topological descriptors［J］.Computers，Materials & Continua，2022，70（2）：3433-3447.

［4］Dong Qing，Sinangil M E，Erbagci B，et al.15.3A 351TOPS/W and 372.4 GOPS compute-in-memory SRAM Macro in 7 nm FinFET CMOS for machine-learning applications［C］//Proc of IEEE International Solid-State Circuits Conference.Piscataway，NJ：IEEE Press，2020：242-244.

［5］栗學磊，朱效民，魏彥杰，等.神威太湖之光加速計算在腦神經網絡模擬中的應用［J］.計算機學報，2020，43（6）：1025-1037.（Li Xuelei，Zhu Xiaomin，Wei Yanjie，et al.Application of Sunway TaihuLight accelerating in brain neural network simulation［J］.Chinese Journal of Computers，2020，43（6）：1025-1037.）

［6］Huang Yipeng.Hybrid analog-digital co-processing for scientific computation［D］.New York：Columbia University，2018.

［7］Ghanem M，Siniora D.On theoretical complexity and Boolean satisfiability［EB/OL］.（2021-12-22）.https：//arxiv.org/pdf/2112.11769v1.pdf.

［8］Salami H O，Bala A.An improved chemical reaction optimisation algorithm for the 0-1 knapsack problem［J］.International Journal of Bio-Inspired Computation，2022，19（4）：253-266.

［9］劉爽.基于SAT的故障樹近似計算和定量分析研究［D］.南京：南京航空航天大學，2019.（Liu Shuang.SAT-based approximate computation and quantitative analysis of fault tree［D］.Nanjing：Nanjing University of Aeronautics & Astronautics，2019.）

［10］Flint O，Wickramasinghe A，Brasse J，et al.A simple proof for a polynomial time 3-SAT solver［EB/OL］.（2019-07-08）.https：//arxiv.org/pdf/1903.10081v7.pdf.

［11］張璐婕，劉暢，張龍，等.一種基于SAT求解器的組合電路重匯聚現象分析方法［J］.計算機科學，2019，46（4）：309-314.（Zhang Lujie，Liu Chang，Zhang Long，et al.Reconvergence phenomena analysis method in combinational circuits based on SAT solver［J］.Computer Science，2019，46（4）：309-314.）

［12］Peng Huanhuan，Zhang Liming，Ye Ziming.An efficient greedy local search algorithm for Boolean satisfiability based on extension rules［C］//Proc of the 2nd International Conference on Mechanical Engineering，Industrial Materials and Industrial Electronics.Piscataway，NJ：IEEE Press，2019：500-507.

［13］馬柯帆，肖立權，張建民，等.加強約束的布爾可滿足硬件求解器［J］.國防科技大學學報，2018，40（6）：105-111.（Ma Kefan，Xiao Liquan，Zhang Jianmin，et al.Hardware Boolean satisfiability solver with enhanced constraint［J］.Journal of National University of Defense Technology，2018，40（6）：105-111.）

［14］Ma Kefan，Xiao Liquan，Zhang Jianmin，et al.Accelerating an FPGA-based SAT solver by software and hardware co-design［J］.Chinese Journal of Electronics，2019，28（5）：953-961.

［15］Somashekar A M，Tragoudas S.Diagnosis of performance limiting segments in integrated circuits using path delay measurements［J］.IEEE Trans on Computer Aided Design of Integrated Circuits and Systems，2017，36（2）：325-335.