改进的模拟退火算法求解规则可满足性问题

张九龙，王晓峰，2，芦 磊，牛鹏飞，程亚南

（1.北方民族大学 计算机科学与工程学院，宁夏 银川 750021；2.北方民族大学 图像图形智能处理国家民委重点实验室，宁夏 银川 750021）

0 引 言

命题逻辑公式的可满足性问题（Propositional Satis⁃fiability Problem，SAT）是计算机理论研究的核心问题之一。SAT 问题在组合电路、逻辑优化、人工智能、数据挖掘等各领域都有着广泛应用。通常意义下的SAT 问题是判定合取范式（Conjunctive Normal Formula，CNF）的可满足性问题，具体可描述为：对于一组给定的布尔变量={,,…,x}，集合中的每个元素称为变元，若变元x在子句中以自身值出现，对应的文字称为正文字，记作x，若变元x在子句中以自身的相反值出现，则对应的文字称为负文字，记作¬x。若干文字的析取构成一个子句C，记作C=(∨∨…∨x)。若干子句的合取构成合取范式（CNF），记作=(∧…∧C∧…∧C)。SAT 问题的判定指判断是否存在一组真值赋值，使得该CNF 公式满足。SAT 问题的求解则是指对于任意的一个合取范式形式表达的命题逻辑公式，找出使得该公式满足的所有布尔变元的真值指派。在SAT问题中，每个子句的长度均为的SAT 问题称为随机⁃SAT 问题。对于随机⁃SAT 问题，进一步加强约束条件，限定每个变元在合取范式中出现的次数恰好为次，形成随机规则(,)⁃SAT 问题。需要注意的是，本文规定的随机规则(,)⁃SAT 问题只规定了变元出现的次数，并未对次中变元正负出现的次数进行限定。

目前，SAT 问题的求解方法主要分为两大类：一类是基于穷举和回溯思想的完备算法，以DPLL（Davis Putnam Logemann Loveland）算法和在其基础上改进的CDCL（Conflict⁃Driven Clause Learning）算 法 为 代 表；另一类是基于局部搜索思想的不完备算法，以随机局部搜索（Stochastic Local Search，SLS）算法、消息传递（Message Passing，MP）算法和演化计算（Evolutionary Algorithm，EA）算法为代表。对于一个给定的CNF 公式，完备算法理论上可以求得公式的解，即使公式无解的情况下也能给出完备证明。缺点也显而易见，当求解大规模问题时，所用的求解时间在最坏情况下会随问题进入难解区域或者变元及子句的增多而呈指数形式增加，求得解的效果也逐渐变差。不完备算法的优点是在处理大规模数据时求解速度相较于完备算法更快，但绝大多数的不完备算法均无法判断SAT 问题的可满足性。完备算法在解决应用类实例时效果明显，对于问题规模较小的应用和组合问题，求解速度甚至快于大多数的不完备算法。完备算法的改进主要是在保证其完备性的同时减少消耗的时间，文献[5]将膜演算的思想加入DPLL 算法中，简化了算法的推理过程。文献[6]提出基于动态奖惩DRPB 的分支启发式算法，通过减小搜索树的规模提升求解器的性能。不完备算法求解速度快，并具有一定的并行性，在处理大规模问题时有较大优势。不完备算法主要分为两个改进方向：一个是与完备算法结合提升其求解过程的完备性；另一个是优化启发式策略，增强算法跳出局部最优解的能力。文献[7]在遗传算法中引入了一种基于DPLL 算法的局部搜索算法，用于求解Max SAT 问题，在多样化搜索和强化搜索之间实现了更好的平衡。文献[8]提出了基于任务分配与调度的GSAT 算法，使用任务分配策略与调度策略共同指导贪心搜索过程，取得了较好的求解效果。

随着大数据时代的到来，数据量呈现爆炸式增长，芯片中晶体管的数量级已从千万级进步到百亿级，计算机的硬件更迭仍满足不了日益剧增的算力需求。因此，不断优化改进求解速度更快的不完备算法是目前SAT 问题求解的一个热门研究方向。在理论研究层面，随机规则(,)⁃SAT 问题限定了每个变元在所有子句中出现的次数恰好为次，比随机⁃SAT 问题更难求解。而现实的工业生产过程中，很多情形下也对某些具体变量的出现次数有要求，如现场可编程门阵列映射芯片的设计与制造。本文在替换的思想上提出了一种新的随机规则(,)⁃SAT 实例生成RRIG 模型（Random Regular Instance Generation Model），通过实验验证了生成模型的正确性和实用性，并改进了不完备算法中的模拟退火算法，得到SARSAT 算法用于求解随机规则(,)⁃SAT 问 题，随 后 将SARSAT 算 法 和 其 他 相关算法在RRIG 模型生成的实例集上进行了测试，验证了算法的有效性。

1 标准模拟退火算法

模拟退火思想最早由Metropolis 在1953 年提出，起初并未引起反响，直到1982 年，Kirkpatrick 等人将模拟退火的思想引入组合优化领域，提出一种用于求解大规模组合优化问题的有效近似算法——模拟退火算法（Simulated Annealing Algorithm，SAA）。模拟退火算法的思想来自热力学与统计物理学中的固体退火过程，其物理原理为：对于与周围环境交换热量而温度保持不变的封闭系统，系统的自发变化总是朝着自由能减少的方向进行，当自由能达到最小值时，系统达到平衡态。在求解组合优化问题时，模拟退火算法能概率性地跳出局部最优并趋于全局最优。

模拟退火算法源于对固体退火过程的模拟，采用Metropolis 接受准则，并通过一组称为冷却进度表的参数控制算法进程，使算法能在多项式时间内给出一个近似最优解。

标准模拟退火算法：

Step1：初始化，任选初始解∈，给定初始温度，终止温度，每个温度下迭代的马尔科夫链长度为n，令迭代指标=0，T=；

Step2：随机产生一邻域解∈()，计算目标值增量Δ=()-()；

Step3：若Δ＜0，无条件接受，令=转Step4；否则，利用Metropolis 准则有条件接受，产生∈(0,1)，若exp( -Δf T)＞，则令=；

Step4：若达到热平衡＞n，转Step5，否则，转Step2；

Step5：=+1，降低T，若T＜算法停止，否则，转Step2。

模拟退火算法发展至今，因其所需要的参数少、对初始解的容忍性及算法本身良好的收敛性，已广泛应用于各个领域求解组合优化问题。文献[11]从数学角度证明了模拟退火算法在固定温度下迭代足够长时间，再将温度降低到下一级，当温度趋近于零时，可获得最低能量状态。若想求得解的效果好，模拟退火算法降温的过程需要足够慢，这就会导致算法执行所需要的时间较长。因此，在使用模拟退火算法求解不同实际问题时需要做出相应的改进。目前对模拟退火算法的改进主要分为两个大的方向：一类是将模拟退火算法与其他算法结合使用，各算法间取长补短；另一类是在标准的模拟退火算法的基础上对退火策略、扰动策略等进行相应的改进，从而提升算法性能。

标准模拟退火算法的算法流程如图1 所示。

图1 标准模拟退火算法流程图

2 规则(k,d)⁃SAT 生成模型

现有的随机正则(,)⁃SAT实例生成模型有文献[17]提出的格局模型、文献[18]提出的严格随机正则SRR 模型等。其中，在格局模型生成的实例中，有可能存在着两种非法情形：某个变元在某个子句中重复出现多次，或者出现若干重复的子句。由于格局模型生成随机实例的方式较为简单，且在证明随机正则(,)⁃SAT 问题的可满足临界值中易于进行相关的概率分析，所以该模型生成的实例通常用来证明可满足临界而非用于求解。在严格随机正则SRR 模型中，为了防止产生非法公式，在生成实例的过程中也会增加一定的限制，因此SRR模型在可满足临界时不易做相关的概率分析。除此之外，两个模型生成的实例均为正负变元出现次数相等或至多差一次的情况，用于研究正则SAT 判定及其相关的证明问题，而非本文中不限变元正负出现次数的随机规则SAT 问题。本文使用替换的思想在两个模型的基础上改进后得到随机规则(,)⁃CNF 实例产生模型——RRIG(,,)模型。该模型包括变元规模、子句长度和变元出现次数等3 个参数，在RRIG 模型产生的实例中，每个子句恰有个不同的文字，每个变元恰好出现次。下面给出RRIG（,,）模型生成随机规则(,)⁃SAT 实例的具体过程。

Input：变元出现次数，子句长度和变元规模。

Step1：置=，=，=0；

Step2：对于每个变元v，随机产生random（0，）个正文字，⁃random（0，）个负文字置于盒子中；

Step3：若中文字个数D＜且文字种类type ＜，转Step5；

Step4：从中不放回的随机选取个文字ℓ,ℓ,…,ℓ组成一个子句C；

Step4.1：若＜-转Step4.2，否则，转Step5；

Step4.2：若选取的文字互不相同，且C没有出现在中，转Step6，否则，=+1，转Step4；

Step5：若1 ＜type ＜转Step5.1；否则，转Step5.2；

Step5.1：随机选取type 个不含C中文字的子句，在每个子句中任意选择一个变元替换C中的变元，转Step6；

Step5.2：随机选取个不含C中文字的子句，从中任选一个文字进行替换，转Step6；

Step6：将C以合取的方式连接到中，置={ℓ,ℓ,…,ℓ}，=+1；

Step7：若＜，返回Step3，否则，输出并结束处理。

Output：随机规则(,)⁃CNF 公式。

在随机⁃SAT 问题中，当≥3 时，问题属于NP⁃完全问题，通过分析算法的计算复杂性，求解NP 复杂类中所有的判定或者优化问题，在最坏的情况下会与⁃SAT（≥3）的判定难度相当。随机3⁃SAT 问题作为随机⁃SAT 问题中最简洁的NP⁃完全问题，在计算机复杂性理论研究中有着重要的作用。因此，将取值为3 得到RRIG（,3,）模型生成随机规则（3，）⁃CNF 实例。

为验证RRIG（,3,）生成模型的准确性，在不同的取值下各生成100 个实例，使用完备SAT 求解算法MiniSat 进行求解得到不同的值下满足实例的比例。为子句个数，为变元个数，以约束密度=作为横坐标，可满足性为纵坐标画出在不同值下实例的可满足性变化，得到RRIG 模型生成的随机规则（3，）⁃SAT 实例的相变如图2 所示。

图2 RRIG（N，3，d）模型生成实例可满足性相变图

目前对于随机3⁃SAT 的相变点，理论上研究表明：3.52 ≤α(3)≤4.489 8，实验表明，α(3)4.267。在随机3⁃SAT 问题中，当＜α(3)时，实例有较大的概率有解；当＞α(3)时，实例有解的概率是较小的；当处于α(3)附近时，随机3⁃SAT 问题是比较难解的。随机规则（3，）⁃SAT 作为随机3⁃SAT 的子类，在添加随机规则后难解程度变大，相变点应相应变小，通过图2 分析可得，利用RRIG(,3,)模型生成实例的约束密度在4.21附近，故此模型是准确的。

3 SARSAT 算法

SARSAT 算法优化模型保留了标准SA 算法的主体框架，针对随机规则(,)⁃SAT 问题，分别对扰动策略、选择策略退火过程等做出了相应改进。

3.1 问题的转化

利用命题逻辑公式中限制性公式的相关理论，可将SAT 问题等价转换为多项式函数优化问题。对于给定的CNF 公式，将∧看成乘，将∨看成加，将变元v视为实参数x，令表示这种转换，用()表示公式的能量函数，则SAT 问题可以转化为一个求相应函数最小值的优化问题。如：

当在一组真值指派σ∈{0,1}下使得能量函数取值为0 时，公式是满足的，称σ为此SAT 问题的一个解。

3.2 扰动策略

在标准模拟退火算法中，每个温度下都需要扰动尽可能多的次数才能保证找到的状态是当前温度下能量较低的状态，这正是模拟退火算法中最影响效率的部分。为了减少模拟退火算法扰动过程消耗的时间，提升算法性能，本文采用了一定的启发式策略来指导扰动过程。对于给定的随机规则(,)⁃CNF 公式，在算法开始前随机给定一组真值赋值∈{0,1}，记作，记公式在赋值下满足的子句集合为，不满足的子句集合为。统计中的变元及其出现的次数，构建一个用于记录变元满足性的矩阵，中每列代表一个变元，行代表变元a第（∈(1,)）次在子句中出现时的满足情况。若满足记为1，不满足记为0。将得到的矩阵记为：

统计下各变元对应满足的子句个数S，则每个变元对应的不满足的子句个数为-S。采用改进的轮盘赌平方策略，各变元被选择的概率如下：

3.3 退火过程

影响模拟退火算法效率的另一个关键是冷却进度表，通常情况下一个冷却进度表包括以下参数：控制参数的初值；控制参数的衰减函数；控制参数的终值。

初值和终值需要根据具体实际问题进行赋值。冷却进度表中最重要的是衰减函数的选择，衰减函数的好坏会直接影响找到解的质量。若温度降低太快，容易导致算法找到的不是全局最优解，反之若温度降低速度太慢，又会影响算法的执行效率。常用的降温策略有快速降温和指数降温，本文在指数降温的基础上增加了回温过程。温度衰减函数如式（4）所示：

式中：为初始温度；为终止温度；为降温因子；为升温因子。取=1000,=0.01，=0.96，=0.6，可得到该情况下的降温曲线如图3 所示。

图3 T0 =1 000,Tf =0.01,δ =0.96,η=0.6 时降温曲线

指数降温的过程不紧不慢，是模拟退火中最常用的降温函数。在指数降温的基础上加入回温过程，若温度降低到一定程度时还未找到最优解，将温度升高，根据Metropolis 准则接受坏解的概率变大，使得算法在求解过程中有多次跳出局部最优的机会，从而更容易找出全局最优解。

3.4 SARSAT 算法

SARSAT 算法流程如下：

Step1：初始化，，、总迭代次数、马氏链长度。随机给定一组真值赋值。

Step2：在每个不满足的子句中采用式（3）选择变元进行扰动，使用贪心策略选择扰动得到的个个体中能量最小的状态记为()，计算能量差值Δ=(-)。

Step3：令=+1，若Δ＜0，则转Step4，否则，若exp( -Δ)≤random(0,1)，转Step2。

Step4：令=,()=()。

Step5：若＜，转Step2。

Step6：根据式（4）的降温过程，判断是否达到最大迭代次数，是就停止，否则，转Step2。

4 实验分析

实验中主机配置为Inter Core i5⁃6300HQ CPU，NVIDIA GeForce GTX960M 显卡，在Python 3.8.2 下编程实现，编程软件为Pycharm，版本为2020.2。

随机规则(,)⁃SAT 是随机⁃SAT 的子集，为验证本文改进的模拟退火算法的有效性，将本文算法SARSAT 与求解随机⁃SAT 问题的不完备算法Walksat、混合蚁群遗传HAGSAT 算法进行对比实验，SARSAT算法使用的初始参数如表1 所示。

表1 算法运行参数

本文使用的实例取自RRIG(,3,)模型产生的不同变元数和变元出现次数的实例，每种情况下各产生20 个实例。对每一个实例，使用三种算法各重复20 次实验并记录实验中求解的平均准确率、无法找到解时的不满足子句占总子句数的比例ns，变元平均翻转次数，所得的实验记录如表2 所示。

通过分析表2 可知，当控制变元出现的次数不变时，随着变元个数的增加，三种算法的执行所需要的时间均变长，变元翻转的次数增多，且三种算法执行所消耗的时间趋势也不同，HAGSAT 算法增长最快、Walksat算法次之、SARSAT 算法增长最慢。在变元数目及子句个数较少时，采用启发策略的HAGSAT 算法与SARSAT算法求解速度均比随机游走算法Walksat 快。因HAGSAT 算法使用了新的初始解生成方式，通过两个阈值控制初始解的盲目性，所以求解小规模SAT 问题时HAGSAT 算法的速度甚至优于随机生成初始解的SARSAT 算法，但是当变元数目进一步增大或者问题逐渐逼近难解区域时，HAGSAT 算法消耗的时间超过了其他两种算法，HAGSAT 算法这种初始解的生成方式增加了算法的执行时间，且随着问题进入难解区域，初始解的优劣对最终解的影响也变小。因为采用的是和相关的启发式翻转策略，SARSAT 算法相较于Walksat 算法中的以固定概率选择翻转和HAGSAT 算法变异杂交等策略，执行效率更高，变元平均翻转次数也最少，SARSAT 算法的求解时间在总体上优于WalkSAT 算法和HAGSAT 算法。在空间复杂度方面，Walksat 算法优于使用信息素矩阵的HAGSAT 算法和使用变元满足性矩阵的SARSAT 算法，随着数据存储技术及计算机硬件的发展，这种以空间换时间和准确率的取舍完全可以接受。SARSAT 算法中的Metropolis 接受准则以及改进后的轮盘赌策略赋予了SARSAT 算法较强的跳出局部最优的能力，对于同一个实例SARSAT 算法的准确率和无法找到解时的不满足子句占总子句数的比例均优于其他两种算法。

表2 实验结果对比

为进一步验证SARSAT 算法翻转策略的有效性，对本文SARSAT 算法与随机扰动的模拟退火算法SASAT算法进行了对比，SASAT 算法的扰动策略为在每个不满足的子句中随机选择一个变元进行翻转，两种算法的对比效果如图4 及图5 所示。

图4 n=120，d=12，m=960

通过对图4 分析可知，对于相同变元数的实例，当变元出现次数较小时，SARSAT 算法与SASAT 算法的求解效率都比较快，温度还未降至就已找到解，且在降温过程中，SARSAT 算法可满足的子句数目比SASAT 算法多。在图5 中，曲线SARSAT⁃代表的是首次降温未找到解后依据式（4）升温再次求解的过程，不难看出，当问题进入难解区域，SASAT 算法已无法找到问题的解，而SARSAT 算法通过回温的过程顺利跳出局部最优进而再一次降温得到局部最优解，验证了本文温度衰减函数的有效性。

图5 n=120，d=13，m=1 040

5 结 语

本文提出了一种随机规则(,)⁃SAT 实例生成模型RRIG（,,）模型，用于生成合法的随机规则CNF 公式，在模拟退火算法求解随机规则可满足问题上对扰动策略、降温策略等做出了相应改进，通过与Walksat 算法和HAGSAT 算法的对比，本文SARSAT 算法在准确率、变元翻转次数和执行时间上优于其他两种算法，可以有效求解随机规则可满足问题。当问题规模进一步增大时，利用模拟退火算法的可并行性来大幅度提高算法性能，是本文接下来的一个改进方向。