Page 122 - 《软件学报》2021年第9期

2746 Journal of Software 软件学报 Vol.32, No.9, September 2021

1 基础知识

1.1 局部搜索
定义 1. 在一个布尔变量集合 V={x 1 ,x 2 ,…,x n }中,每个变量呈正、负两种文字形式 x i 和¬x i 以析取的形式存
在于 CNF(conjunctive normal form)公式的每个子句 C i 中,公式中的每个子句之间是合取的.找到一个或多个解
释能使 CNF 公式为可满足的真值指派过程,称为 SAT 求解.
SAT 问题的求解是按照某种特定规则对变量进行选取、赋值和剪枝等过程,找到可满足的解释.完备的算
法如 DPLL,其功能在于不仅可以判断子句集的可满足性,而且可以找到可满足的解.局部搜索作为不完备的方
法采取完全不同的方式对 SAT 问题进行求解,该方法通过不断变换部分子句空间所有变量赋值使得可满足的
子句不断增加,最终达到子句集可满足的目的.当处理不可满足的问题时,由于子句集无解而使变量赋值无限地
变换下去.因此,局部搜索只能求解可满足的子句集,且其求解效率远高于完备的算法,却无法处理不可满足的
子句集.
1.2 扩展规则
传统的归结方法是通过归结出空子句来判断子句集不可满足;而作为归结的互补方法,扩展规则是通过对
CNF 公式中的子句能否扩展出所有极大项来判断其可满足性.其基本定义如下.
定义 2. CNF 公式中的一个子句 C,变量 l 的文字形式不在 C 中出现.有 D={C∨l,C∨¬l},则称 C 到 D 的过程
为扩展规则,D 是子句 C 关于变量 l 扩展后的结果.
定义 3. 若一个子句包含所有变量对应的正文字或负文字之一,则称该子句为变量集的一个极大项.
初始的扩展规则推理方法是通过计数每个子句所能扩展出的极大项个数,利用容斥原理计算所能扩展出
n
极大项总数.如果极大项个数是 2 (n 为变量个数),则 CNF 公式是不可满足的;否则是可满足的.这种完备算法的
缺点在于:其处理的 CNF 规模十分有限,当子句数超过一定阈值,将会造成内存溢出.李莹等人提出的 NER 算法
通过一定次序判断当前极大项 T 是否能被 CNF 公式中的子句扩展出来:当所有极大项都能被扩展出来时,子句
集不可满足;当存在至少一个极大项不能被扩展,则子句集可满足.该算法的求解效率远优于 ER 和 IER 算法,但
缺点在于机械地变换极大项,暴力的求解方式满足了算法的完备性,却丢失了很多启发式信息.杨洋等人提出的
ERACC 算法基于局部搜索的格局检测方法,通过得分机制选取变量,根据变量的邻居关系精确格局信息,并通
过双向半扩展规则来限制变量的选取范围.该算法在时间复杂度和空间复杂度上都有了很大的改进,并且利用
了局部搜索的高效性,使求解可满足问题的求解效率达到了质的飞跃.
1.3 基于精确格局检测的扩展规则算法

基于局部搜索的扩展规则推理方法的本质在于:以寻找极大项空间不可扩展的极大项为目标,利用贪心策
略限定极大项空间,以变量的邻居变量设定格局信息,从而减少了冗余搜索步骤,牺牲了算法完备性,从而达到
了高效求解的效果.
ERACC 算法的精髓在于对极大项中反转变量的选择,通过最大左度和最小右度的概念,限定两集合中的变
量.如果集合为空,则退一步选择得分高的变量取反.精确了变量的选择直接控制了极大项的变换,使得推理过
程更加精确(算法的具体流程见文献[18,19]).但是算法仍存在以下不足:初始极大项的选择并没有明确的启发
式;串行的处理也使得 ERACC 算法无法发挥出极致的效果;忽略了预处理技术,使子句集没有化简的过程.下文
将针对以上问题提出 PERACC 算法,使求解的性能发挥到极致.

2 PERACC 算法

传统的基于扩展规则的并行推理方法将子句集的极大项空间分解为若干个子空间,并对其进行逐一求解.
这种并行方式并未加入启发式信息,使得分割空间无层次.即使分割的子空间彼此毫无关联,但整体推理的空间
复杂度并无降低.