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

李壮 等:基于局部搜索的并行扩展规则推理方法 2747

本文提出的并行处理是一种结合了对解空间化简的预处理方法.在选择特定的变量之后,对原子句集进行
化简,化简后的子句集与原子句集是逻辑等价的,这也极大地降低了对整个子句集求解的空间需求;并在
ERACC 算法中加入了对初始值的赋值限制,改变了 ERACC 对初始值赋为 1 的单调做法,使求解器整体求解能
力得到了较大地提升.
2.1 CPVI算法

我们通过选取变量的启发式算法,对出现在每个子句中的文字赋予权值.从文字出现在各个子句中的累计
次数计算出得分最高的变量.首先,遍历原始子句集获得所有文字的数组,从数组中选取最大数对应的变量.如
果同等数量的变量有若干个,那么从中随机选取需求个数作为初始变量,变量个数由所划分的解空间参数决定.
变量选取算法如下,其中,vs=(var,score)表示变量及对应的得分,其中,var 表示变量,score 表示变量的得分.
算法 1. 计算选取的变量 CPVI(computing the picking variables initially).
输入:CNF 公式 F={C 1 ,…,C m },选取变量个数α;
输出:CNF 公式 F 中包含最多文字的前α个变量的集合 result.
1 result←∅,vs←∅;
2 {v 1 ,v 2 ,…,v n }←getAL(F) //函数 getAL 返回 CNF 公式 F 中所有变量的集合
3 FOR (i←1; i<n+1; i++) //初始化数组 score
4 vs i .var←v i ;
5 vs i .score←0;
6 FOR (i←1; i<n+1; i++) //对每个变量循环
7 FOR (j←1; j<m+1; j++) //对每个子句循环
8 IF vs i .var∈C j
9 THEN vs i .score=vs i .score+1; //数组 score 的第 i 个元素表示第 i 个变量的得分
10 sv←sort(vs,n); //函数 sort 根据 score 域对数组 vs 进行从大到小的排序
11 ns←{sv α .var};
12 i←α+1;
13 k←1;
14 IF sv α .score=sv i .score
15 THEN
16 WHILE (i<n+1 and sv α .score=sv i .score)
17 ns←ns∪{sv i .var};
18 i←i+1;
19 i←α−1;
20 WHILE (i>0 and sv α .score=sv i .score)
21 ns←ns∪{sv i .var};
22 k←k+1;
23 i←i−1;
24 svars←random(ns,k); //函数 random 返回从集合 ns 中随机选取 k 个元素
25 result←{sv 1 .var,…,sv α−k .var}∪svars;
26 ELSE result←{sv 1 .var,…,sv α .var};
27 RETURN result.
算法 1 采取一种遍历求和排序的方式来计算各个变量的得分集合,从而选取权重最高的变量作为化简子
句集的初始变量.算法第 2 行表示程序遍历了整个子句集 F 并统计了所有变量集合;第 3 行~第 5 行对所有的变
量及其得分清零;第 6 行~第 10 行分别描述了对所有变量和每个变量在各个子句中的双重循环,得到变量集合