基于改进连续时间动态系统的模拟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.