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

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

11 RETURN {l 1 ∨l 2 ∨…∨l n }. //返回的是一个初始的极大项
算法 3 中,i 代表初始的极大项,通过遍历子句集得到 F 中的变量数 n,再根据每个变量所对应的文字统计其
正、负文字出现的个数,n(l i )表示变量对应的文字总个数.第 5 行~第 10 行是一个循环.根据正负文字出现的个数
与变量对应的文字总个数,计算对应极大项中该变量应该赋值的概率,即有指向性地调整了变量赋值的概率.逐
一对变量赋值之后,当赋值变量的个数完成了第 n 个后,说明初始极大项已经产生,算法结束.有针对性地选择初
始极大项,会使下一步的推理更加精准,提高了推理效率.
2.4 PERACC算法
结合了以上算法,基于 ERACC 算法,我们提出了基于精确格局检测的并行扩展规则算法,算法过程如下.
算法 4. 基于精确格局检测的并行扩展规则算法 PERACC(parallel extension rule based on accurate
configuration checking).
输入:CNF 公式 F,MaxTries,选取变量个数α;
输出:不可扩展极大项 T′或最长尝试次数 MaxTries.
1 result←CPVI(α) //选择变量数组
α
2 num←2 ; //解空间总数
3 FOR (i=0; i<num; i++)
4 startThread(i,F′,T); //函数 startThread 启动解空间 i,F′为化简后的子句集,T 为当前极大项
5 T←SIMT(F′) //调用 SIMT 计算各个解空间的初始极大项
6 WHILE j<MaxTries DO
7 IF CanBeExpend(⋅) THEN RETURN T //判定当前极大项是否能被扩展
8 Compute the Candidate Set(left,right)
9 P={v|Score(v)>0 and conf[v]=1}
10 IF P≠∅ THEN
11 IF left≤rignt THEN
12 S={v|Score(v)>0 and left≤0≤rignt and conf[v]=1}
13 IF S≠0 THEN x←v∈S with largest Score
14 ELSE x←v∈P with largest Score
15 ELSE x←v∈P with largest Score
16 ELSE x←SWT(F,T,W[⋅],time[⋅])
17 T′←T/ref(T,x)∪¬ref(T,x)
18 j++
19 WHILE (1) DO
20 FOR (i=0; i<num; i++)
21 IF EndThread(i) //函数 EndThread 判断解空间 i 是否计算完
22 THEN RETURN resultThread(i). //函数 resultThread 返回解空间 i 的结果
算法 PERACC 的执行过程大致如下:第 1 行~第 4 行通过调用 CPVI 算法选择初始变量,通过变量选择的数
量,得到分解解空间的数量,并对各个解空间进行化简,然后对各个解空间进行求解;第 5 行调用算法 SIMT 来计
算各个解空间的初始极大项;第 6 行~第 18 行是调用 ERACC 算法对每个解空间的求解,其详细过程可参考文献
[18,19];第 19 行~第 22 行是一个死循环,当各个解空间中,某一个解空间找到了扩展不出的极大项,那么跳出该
循环.
3 实验结果与分析

本节对算法 PERACC 算法进行实现,并且将其与扩展规则领域主流的求解器 SER,ERACC 以及国际主流