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

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

间作为判断的标准.我们提出了 PERM 算法来解决这一问题.
PERM 算法过程如下:
算法 2. 并行扩展的推理方法 PERM(parallel extensionrulereasoning method).
输入:CNF 公式 F={C 1 ,…,C m },F 的极大项 T,选择变量个数α;
输出:不可扩展的极大项 T 或最大尝试次数 maxTries.
α
1 num←2 ; //解空间总数
2 FOR (i=0; i<num; i++)
3 startThread(i,F,T,ERACC); //函数 startThread 启动解空间 i,调用 ERACC 算法
4 WHILE (1) DO
5 FOR (i=0; i<num; i++)
6 IF EndThread(i) //函数 EndThread 判断解空间 i 是否计算完
7 THEN RETURN resultThread(i). //函数 resultThread 返回解空间 i 的结果
算法 2 给出在极大项子空间中分割原始极大项解空间的并行算法 PERM.首先输入原 CNF 公式和已选取
α
的变量,预处理程序通过二进制方法将变量的 2 种析取将子句集的极大项空间分解为 thread num 个独立的子空
间,并记录每个子空间的返回结果,然后对每个极大项子空间并行地调用 ERACC 算法进行极大项的判定.当某
一个极大项子空间 EndThread(i)中返回的结果为 SAT,即该子空间中存在某个极大项在规定时间内不能被扩展
出来的子句,则子句集是可满足的.将该结果返回至主程序,推理过程结束.

2.3 SIMT算法
由第 1 节我们可知,NER 和 ERACC 两种算法都是以寻找子句集扩展不出的极大项为目标来进行推理的,
所以我们采取的途径是变换和调整极大项的模型.在 ERACC 中已详细地说明了如何去变换调整极大项,忽略
了对初始极大项的重视,采用了单纯的对初始极大项中没个变量赋值为 1.初始的极大项中,变量的赋值在整个
推理过程中占据重要的位置.如果没有针对性地给初始极大项赋值,则会在求解过程中走很大的弯路,间接地增
加了冗余的推理过程.
为了使推理过程更直接、高效,我们提出了 SIMT 算法,有针对性地解决对初始极大项中变量赋初始值的选
择.由于极大项中的每个变量可以赋值为正和负两种文字形式,而每种文字形式的赋值概率为 50%,我们提出的
算法是每个变量根据原子句集中文字出现的比率来确定初始极大项中变量的取值概率.实验结果表明,我们的
策略是有效的.
SIMT 算法过程如下.
算法 3. 选择初始极大项方法 SIMT(selection of initial maximum term).
输入:CNF 公式 F;
输出:初始极大项 T.
1 i←1;
2 n←getNumLiteral(F); //返回 CNF 公式 F 的变量数目
+
3 {, ,..., }ll 2 + l n + ←getPosLiteral(F); //返回 CNF 公式 F 中每个正文字的个数
1
−
4 {, ,..., }ll 2 − l − n ←getNegLiteral(F); //返回 CNF 公式 F 中每个负文字的个数
1
5 WHILE i≤n DO
−
+
6 ln i ← l + l ;
i i
+
7 p i ← l /n(l i );
i
−
8 q i ← l /n(l i );
i
9 l i ←random(p i ,q i ); //随机返回 p i 或 q i
10 i←i+1;