基于改進(jìn)連續(xù)時間動態(tài)系統(tǒng)的模擬SAT求解器

趙海軍 陳華月 崔夢天

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

關(guān)鍵詞：布爾可滿足性問題；連續(xù)時間動態(tài)系統(tǒng)；模擬設(shè)計；輔助變量；數(shù)字驗證；加速性能

中圖分類號：TP331?? 文獻(xiàn)標(biāo)志碼：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 引言

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

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

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

1 k-SAT問題及改進(jìn)的連續(xù)時間動態(tài)系統(tǒng)

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

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

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

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

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

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

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

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

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

2 系統(tǒng)方程的模擬硬件設(shè)計

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

2.1 信號動態(tài)電路

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

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

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

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

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

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

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

2.2 輔助變量電路和數(shù)字驗證電路

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

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

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

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

2.3 可替代的AVC設(shè)計

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

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

3 方案評價

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

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

算法1 歸結(jié)算法

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

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

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

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

4 結(jié)束語

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

參考文獻(xiàn)：

［1］蔣東華，劉立東，王興元，等.基于細(xì)胞神經(jīng)網(wǎng)絡(luò)和并行壓縮感知的圖像加密算法［J］.圖學(xué)學(xué)報，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］張小紅，廖琳玉，鐘小勇.一種憶阻細(xì)胞神經(jīng)網(wǎng)絡(luò)的電路設(shè)計方法：中國，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］栗學(xué)磊，朱效民，魏彥杰，等.神威太湖之光加速計算在腦神經(jīng)網(wǎng)絡(luò)模擬中的應(yīng)用［J］.計算機(jī)學(xué)報，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］.南京：南京航空航天大學(xué)，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求解器的組合電路重匯聚現(xiàn)象分析方法［J］.計算機(jī)科學(xué)，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］馬柯帆，肖立權(quán)，張建民，等.加強(qiáng)約束的布爾可滿足硬件求解器［J］.國防科技大學(xué)學(xué)報，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.