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

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

的得分数组 vs i .score,并对其进行排序;第 12 行~第 24 行表示当出现得分均等的若干个变量时,从中随机选取所
需个数变量;最后输出所选择的变量.
变量得分的计算,令 F 为 CNF 公式,C i ={l 1 ,…,l k }为子句集中任意子句(i∈(0,m]),m 为子句数,W i 为子句相关
联文字的权值.则变量 v 基于 F 的得分函数为
m
Score ()v = ∑ |δ (, ) |C l × W i .
i
i= 1
在以上公式中,δ为二元谓词特征函数,代表多值逻辑的取值.令 l 表示在子句 C i 中变量 v 所对应文字的取值.
δ的具体定义如下:
⎧ 1, C中的 l为正文字
δ (, )Cl = ⎨ i .
i −
⎩ 1, C中的 l为负文字
i
以上公式给出了变量得分的计算方式,基本思想为:根据文字出现在子句中的形式取相应的值.正文字取
1(变量所对应文字为 l时取 1),负文字取−1(变量所对应文字为¬l 时取−1).通过求和计算累计变量的得分,根据得
分将变量排序,进而选取所需变量.该方法的时间复杂度是线性的,因此,该预处理方法所需时间在求解的过程
中所占比重是极小的.
例 1:令 CNF 公式 F={A∨C∨¬D,¬B∨¬G∨H,¬A∨E∨G∨¬H,C∨E∨H,¬D∨G∨¬H},在该测试用例中,每个变量
相对应的文字权值 W i 为 1,则变量的得分如下:
• Score(A)=|1×1|+|0×1|+|(−1)×1|+|0×1|+|0×1|=2;
• Score(B)=|0×1|+|(−1)×1|+|0×1|+|0×1|+|0×1|=1;
• Score(C)=|1×1|+|0×1|+|0×1|+|1×1|+|1×1|=2;
• Score(D)=|(−1)×1|+|0×1|+|0×1|+|0×1|+|(−1)×1|=2;
• Score(E)=|0×1|+|0×1|+|1×1|+|1×1|+|0×1|=2;
• Score(G)=|0×1|+|(−1)×1|+|1×1|+|0×1|+|1×1|=3;
• Score(H)=|0×1|+|1×1|+|(−1)×1|+|1×1|+|(−1)×1|=4.
由例 1 可以看出:给定 CNF 公式 F 中,所有文字的权值为 1,在对变量选择的过程中扫描一次即可得知变量
的得分.在选取变量阶段,我们选取得分最高的变量(例 1 中的变量 F).在硬件条件允许的条件下,我们可以选择
多个变量.如果我们选择 3 个变量,那么会根据得分依次选择变量 G 和变量 H,而第 3 个变量的选取则在得分相
等的变量{A,C,D,E}中随机选取一个.
我们的目的在于对原解空间进行最大程度化简,因此选择了得分最高的变量作为初始变量.最理想的情况
是存在某个变量出现在每个子句中,这样可以最大程度地降低子句集规模,得到的问题规模最小.即:在预处理
阶段约简了原子句集,其约简后的结果与原子句集是逻辑等价的.
定理 1. 预处理阶段,化简后的子句集与原子句集是逻辑等价的.
证明:固定了极大项中的文字之后,原子句集中带有互补文字的子句可直接忽略,因为这样的子句是无法扩
展出当前极大项的;而带有相同的文字可以忽略不计,只看除了该文字剩余部分的子句.这样,剩余变量的模型
组成了新的极大项,与化简后的子句集相对应,即,同原极大项和原子句集是逻辑等价的.
例 2:令 CNF 公式 F={A∨B∨C∨D,¬A∨B∨¬C∨E,¬A∨¬B∨¬G,¬A∨B∨¬D∨¬E,B∨C∨¬D∨G},按照算法 1 选取
变量,我们应选择的变量为 A 和 B.如果我们单看其中的一个子空间,变量取值为¬A 和 B,那么化简的原子句集为
F′={¬C∨E,¬D∨¬E,C∨¬D∨G},新的解空间是由变量{C,D,E,G}所组成的极大项空间.
由例 2 可以看出:在保证了逻辑等价的前提下,化简后的子句集规模已经远远地小于原子句集的规模.实验
证明:不论在时间还是空间上,都有了很大的提高.
2.2 PERM算法
选择变量的目的在于化简解空间,而并行的目的是基于化简基础上能够全面地对子句集求解.由于选择的
变量组合的不同,对子句集化简的程度也不同.基于该问题,我们会选择几种化简后,求解效率最高的那个子空