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

黎铁军，马柯帆，张建民

(国防科技大学计算机学院，湖南 长沙 410073)

1 引言

可满足性问题SAT(SATisfiability problem)作为最著名的NP完全NPC(Non-deterministic Polynomial Complete)问题之一，被广泛应用于理论研究和实践领域。许多困难的组合问题，包括硬件与软件的形式化验证、人工智能、运筹学、计算生物学、密码学、数据挖掘和机器学习等方向出现的问题，都可以用基于SAT的技术来解决。自从关于在可重构硬件上实现SAT求解器的综述[1]发表以来，基于硬件的SAT求解器获得了飞速的发展。最坏情况下，SAT问题求解时间呈指数增加，因此，近年来针对如何利用FPGA固有的灵活性和并行性高效求解SAT问题成为业界研究的热点。

SAT问题求解的最终目的是获得高效正确的判定。SAT求解器在不断追求高效算法的同时，不可避免地会遇到一些问题[2]。对软件求解器来说，一些求解器尽管性能优异，但求解算法过于复杂，研究人员需要大量专业知识去理解概念的正确性和算法运行机制。一些已经解决的问题或许还存在更优的求解方法。此外，一些求解器一味地追求其性能而忽视了算法的完备性，甚至正确性。对硬件求解器来说，软件求解器中新的启发式和数据结构的应用对硬件SAT求解器的加速策略作出了显著贡献。然而，尚不清楚硬件SAT求解方案的总体进展是否跟上了日益复杂和高效的软件求解器的快速进步。基于硬件的SAT求解器仍面临诸多挑战[3]。

本文重点研究了基于随机局部搜索SAT求解器的算法与实现，提出了基于FPGA的并行多线程求解器pprobSAT+。但是，与以往单线程求解器不同的是，pprobSAT+是线程级的硬件并行求解器，由于使用多线程执行的策略，避免了搜索过程中的等待延时，提高了求解效率。实验结果表明，相比于单线程求解器，本文提出的三线程并行求解器的求解效率有显著提高，最大可达2.4倍的加速。

2 研究现状

求解SAT问题有许多不同的算法，这些算法基本上可以分为2类：完全算法和不完全算法。完全算法总是可以找到使公式满足的解或者推断出问题不可满足。其优点是能准确判定SAT问题是否满足，当实例无解时可以给出完整的证明，但其缺点是解空间的复杂度会随着问题规模的不断增大呈指数增长，因此，早期的完全算法仅仅适合求解小规模的SAT问题，且计算效率不高。

不完全算法主要是基于局部搜索算法[4]和遗传算法[5]。文献[6,7]分别提出了一种基于加强约束和概率分布函数的FPGA SAT求解器。通常，不完全算法不能保证在指定的步骤内找到问题的解。当解存在时，意味着SAT问题可满足，反之，不能说明该问题不可满足。

近年来，完全算法在解决布尔可满足性等许多现实问题方面取得了很大的进展，但由于搜索空间的急剧增大，它们往往不能很好地扩展。解决组合爆炸问题的一种方法是牺牲完备性，使用这种策略的最著名的方法是局部搜索算法。通常，局部搜索策略从初始赋值开始，该初始赋值可以是随机生成的，也可以是启发式生成的。然后，根据目标函数将搜索总是转移到较好的邻域，如果目标达到或找不到更好的解，则终止搜索。与完全算法相比，不完全算法一般速度更快，单位时间迭代次数更多。对于某些类型的SAT问题，如3-SAT，特别是较大规模的3-SAT，其效率更高。

3 并行FPGA SAT求解算法

SAT求解的流程如图 1所示。预处理器使用纯文字规则对SAT实例进行化简，这个过程不会改变实例的可满足性[8]。此外，预处理还产生多组当前赋值不满足的子句、变元初始赋值。

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

对软件求解器来说，并行求解算法主要是使用不同的种子和参数在不同的 CPU 核上执行多个任务，以达到并行求解的目的。本文提出的基于不完全算法的并行多线程求解器就是基于这个概念，它是文献[7]提出的基于概率分布的单线程FPGA SAT求解器在实现方式上的进一步延伸。本文提出的基于不完全算法的并行多线程求解器的基本思想是，对相同的SAT实例，主机提取的地址映射表以及子句映射表是一致的。基于pprobSAT+的并行硬件求解器，最直观的处理方式是在同一块或者多块FPGA中复制多个完整的求解器。在算法求解过程中，这些求解器使用不同的策略(如不同的初值、随机数生成器产生的不同地址)对同一实例进行并行求解，任何一个求解器找到问题的解即搜索停止，问题可满足。反之，只有在规定的时间或者步数内所有求解器均不能找到解，搜索才能停止。然而正如文献[2]所描述的，算法在搜索的过程中，要最终确定当前赋值不满足的子句中实际翻转的变元，需要临时翻转子句寄存器中的3个文字，评估各文字相关的子句并计算对应的break-value值。由于算法是顺序执行，因此在搜索的不同阶段，势必会使电路中的某些部件处在空闲状态。若采用简单的复制多个求解器的方式必然会带来很大的资源浪费，特别是导致片上存储器的大量浪费。利用多线程策略，对相同的实例尝试更改初始赋值，以实现MAX-TRIES搜索，不同线程均对同一地址和子句映射表进行数据交互，则会大幅度地减少片上存储器的资源开销，并且由于使用多线程策略，每秒总翻转量将会成倍地增加，有更大的概率在规定的时间内找到问题的解(如果存在的话)。多线程求解示意图如图2所示。

Figure 2 Multi-thread solving图2 多线程求解框图

Figure 3 pprobSAT+ achitecture图3 pprobSAT+求解器结构

求解器硬件结构如图3所示。在pprobSAT+并行求解器中，搜索开始前，主机根据实例提取相关数据：(1)给定问题的子句数据，(2)对变元的多组初始赋值，图3中Nv表示变元数量；(3)对应赋值下的不可满足的子句信息，并将数据下载到电路中。其中，多组初始赋值和不可满足子句是用于多线程搜索的。子句数据存储在地址和子句映射表中，不同的初始赋值存储于子句评估模块中的变元表中(每个变元表存储一组初始赋值)。对于XILINX Virtex-6 FPGA (XC6VHX565T)芯片，其内部包含多达912个片上RAM(容量为36 Kb)，每个RAM可以拆分成2个独立的18 Kb RAM块使用,因此在未使用片外存储器的情况下最多可求解36 Kb的变元，若要求解更大规模的实例则需要多个RAM块。多组当前赋值下不可满足的子句存储在不同的不可满足子句存储器中。同样地，pprobSAT+求解器主要用于求解3-SAT问题。

在pprobSAT+并行求解器中，选择缓存器存储的当前赋值下不可满足的子句是随机的。电路中不可满足子句寄存器的大小为4 096。假设不可满足子句寄存器中的子句数为m,此时，需要在0到m中生成一个随机数来作为地址选择寄存器中当前赋值下的不可满足子句。随机数产生模块由D触发器和若干个异或门组成的线性反馈移位寄存器来实现，产生一个21 bit的随机数NR，为了避免搜索过程中的除法运算，预先计算出1/m(m=1，…，4 095)的值，并将值左移20位的结果存储在片上RAM中。最终不可满足子句寄存器中的地址r由NR对m取模得出。

4 实验结果与分析

并行FPGA SAT求解器的主要目的是使用当前先进的硬件平台，以更高效、便捷的方式求解超大规模的SAT实例。由于实例提取的子句信息、变元赋值等均存储在FPGA的片上RAM，因此随着实例规模的增大，求解器消耗的逻辑资源会急速增长。对XILINX Virtex-6 FPGA (XC6VHX565T)芯片，在单线程的情况下片上RAM的使用率可达到95%。对pprobSAT+并行求解器，势必需要更大规模的FPGA才能实现，考虑到实验的首要目的是验证求解器的可行性和可扩展性，以下实验来源于功能仿真结果。实验中预处理部分均在Intel(R)Core(TM)i5-6400 64-bit 2.7 GHz CPU 8.0 GB RAM和Linux Ubuntu-14.04环境下编译和执行。求解器使用Verilog硬件描述语言，在ISE 14.7环境下开发，并使用Mentor Graphics公司的Modelsim SE-64 10.4进行仿真实验。

由于pprobSAT+求解器是一个基于不完全算法求解器，因此选取的测试用例是可满足的实例，为了便于功能仿真过程中实验结果的观察与分析，本文选取SATLIB Benchmark Problems小规模的随机实例uf50-01测试。问题规模为50个变元、218个子句。虽然实例规模较小，但从问题求解的难度来说，实例子句变元比均处于临界值4.26左右，其不可满足和可满足的概率几乎是相等的，属于难解的一类问题集。

本文从 2011 年 SAT 竞赛的测试基准库[9]中选取 4个小型和2个中型的随机实例进行验证。三线程并行求解器pprobSAT+相对单线程求解器 probSAT+[6]的性能增益如表1所示。probSAT+求解器系统结构与预处理方式类似于pprobSAT+，区别在于前者为单线程求解。表1中是软件仿真结果，考虑到对随机产生的地址来说，并不能做到完全随机，最终的地址由伪随机数产生，也就是说在使用的种子不变的情况下，每次产生的随机数是确定的，为了更公平地比较求解效率，测试中对每个实例独立运行 5 次，所得的数据为 5次测试的平均值。不难发现，当实例规模很小时，产生的当前赋值下不可满足的子句数相对较少，多线程并行求解器并不能获得很高的加速比，随着实例规模的不断增大，相比单线程求解器，多线程并行求解器可获得超过2倍的加速比。

Table 1 Performance comparison表1 性能对比

5 结束语

本文提出了一种在 FPGA 上实现并行多线程 SAT 求解器的新方法pprobSAT+。在求解的过程中，3个独立的线程被同时执行，以使并行和流水线电路具有很高的求解性能。当实例规模满足所有的数据都存储在 FPGA 片上存储器时，本文提出的求解器pprobSAT+能获得最大性能。若能将部分数据存于片外存储器，则能大大提高求解器处理问题的规模。本文仅对提出的并行多线程求解器进行了初步的功能仿真，求解器时序仿真以及布局布线方面的优化还需要进一步分析。除此之外，该求解器的另一个局限性是当前的最大值设置为30，若要求解具有更大规模的SAT问题，需要进一步研究流水线的执行方式。为了达到这些目的，需要对电路进行改进，使其能够动态地改变流水线的长度，这也是未来研究的方向之一。