基于知识编译的推理方法主要通过结合离线编译和在线推理求解重复性推理问题。离线编译阶段利用编译算法将知识库编译为易处理目标语言，在线推理阶段则利用适用于易处理目标语言的多项式推理算法实现推理问题的高效求解。可分解否定范式(DNNF)能够应用于可能性推理、规划、诊断等多个领域内推理问题的求解，针对该目标语言，Darwiche设计了能够将任意子句集编译为DNNF的知识编译方法^[1-2]，并给出了知识编译图谱^[3]。模型计数是计算知识库模型个数的问题，针对该问题，Koriche等^[4]提出了基于Affine决策树的高效求解方法，并研究了基于Affine语言族的推理方法。约简的SDDs(sentential decision diagrams)语言是OBDDs(ordered binary decision diagrams)目标语言的超类目标语言，Broeck等^[5]针对该语言研究了多项式时间内的推理方法。通过引入蕴含文字的概念，Lai等^[6-7]提出了带有蕴含文字的有序二元决策图，是一类新的知识编译语言，同时还基于合取的可分解性设计了几种新的知识编译目标语言。Lagniez等^[8]针对Decision-DNNF语言设计了一种编译器，具有较高的编译效率和编译质量。Amarilli等^[9]研究了知识编译中的连接宽度和结构。上述研究提高了相关知识编译目标语言的应用范围、表示能力以及编译算法的性能。

扩展规则推理方法(extension rule, ER)是Lin等^[10-11]于2003年提出的一种推理方法。基于扩展规则，Lin等^[10]提出了KCER算法，可以将任意子句集编译为等价的EPCCL理论。针对KCER算法中的子句选择过程和子句扩展过程，谷文祥等^[12]分别设计了MCN启发式策略和MO启发式策略，使KCER算法的编译效率和编译质量得以大幅度提升。刘大有等^[13]证明了EPCCL理论能够在多项式时间内支持知识编译图谱中的全部8种查询操作，并基于扩展规则和DPLL算法设计并实现了高效的EPCCL理论编译器C2E。刘磊等^[14]提出了超扩展规则，并设计了3种EPCCL理论编译算法：UKCHER算法^[15]、DKCHER算法^[15]和IKCHER算法^[16]，其中，DKCHER算法是目前为止表现最好的EPCCL理论编译算法。EPCCL理论是一种具有较强竞争力的知识编译目标语言，提高其编译器的编译效率和编译质量具有重要意义。

本文基于规约规则研究了EPCCL理论中相邻子句的约简，并提出了RACE算法。利用RACE算法能够有效约简DKCHER算法产生的中间结果EPCCL理论和最终结果EPCCL理论中所有满足规约规则的相邻子句，基于此本文设计并实现了imp-DKCHER算法。

1 超扩展规则

本文中，用变量集V(F)和变量集V(C)分别存储子句集F和子句C中出现的所有变量，用极大项集J_N(C)和极大项集J_N(C)分别存储子句C和子句F在变量集N上所能扩展出的所有极大项。本文所研究的子句集中不包含重言式。语义等价用‘≡’符号表示，对于单个子句C，C≡J_N(C)。

扩展规则使用单个变量扩展单个子句^[10]，为了充分挖掘子句间的关联关系，刘磊等^[14]提出了超扩展规则，能够在2个子句上完成扩展操作。

定义1(超扩展规则, Hyper extension rule)^[14]。给定2个子句C和A，D={C∨A, C∨A}，其中V(C)∩V(A)= $\emptyset $，将C到D的推导过程称为超扩展规则，D中的元素为C应用超扩展规则的结果。

在定义1中，应用超扩展规则所得结果中包含$C \vee \neg A $这样的非子句形式(C∨A为标准子句形式)，为了使所得结果仍然是一个子句集，文献[14]中利用互补展开将$ C \vee \neg A $转化为两两子句互补的子句集。

超扩展规则具有以下性质^[15]：基于超扩展规则可以计算2个子句所能扩展出极大项的差集，并结合互补展开可以将计算结果保存为EPCCL理论。

在定义1中，为了使超扩展规则所得结果有意义，假设A|≠C，且A和C不包含互补文字对，则D={C∨A, C∨A}≡{C∨A, C∨(V(A)-V(C))}，其中，C∨A代表了J_N(C)∩J_N(A)，而{C∨(V(A)-V(C))}则代表了J_N(C)-J_N(A)。

定义2(EPCCL理论)^[11]。若子句集F中任意2个子句之间均包含互补文字对，则称F是一个EPCCL理论。

定义3(规约规则)^[13]。给定2个互补子句C₁=l₁∨…∨l_n∨l和C₂=l₁∨…∨l_n∨l，称从C₁∧C₂到l₁∨…∨l_n的操作为规约规则，并称l₁∨…∨l_n为对C₁和C₂使用规约规则的结果。

给定任意子句集F={C₁, …, C_m}，令N表示F中出现的变量集。DKCHER算法利用超扩展规则的性质计算J_N(□)-(J_N(□)-J_N(C₁)-…-J_N(C_m))，进而得到与F等价的EPCCL理论^[15]。显然，DKCHER算法分2步执行：1)计算J_N(□)-J_N(C₁)-…-J_N(C_m)，并将计算结果保存为EPCCL理论。假设第一步所得结果为{E₁, …E_h}，则2)计算J_N(□)-J_N(E₁)-…-J_N(E_h)，所得结果是与F等价的EPCCL理论。

2 相邻子句规约

根据DKCHER算法的执行流程可知，DKCHER算法在第一步计算得到的结果是一个EPCCL理论E={E₁, E₂，…，E_h}。在第2步计算时，第1步计算得到的EPCCL理论将作为输入子句集完成J_N(□)-J_N(E₁)-…-J_N(E_h)计算，显然E的规模能够影响第2步计算的效率，若能有效减少E的规模，则能提高DKCHER算法的整体编译效率。同时编译质量是评价知识编译算法的重要指标，若能有效减少DKCHER算法输出EPCCL理论的规模，则能提高DKCHER算法的编译质量。

刘大有等^[13]基于规约规则设计了多项式时间的规约算法REDUCE，能够规约EPCCL理论中所有满足规约规则的子句，然而该算法在EPCCL理论上完成规约操作，而通常EPCCL理论的规模远大于输入子句集，因此该算法依旧需要较长的运行时间，在文献[13]中，对于子句数为100、变量数为30、子句长度为4的实例，REDUCE算法的运行时间是知识编译算法KCDP 2倍以上。因此结合REDUCE算法会大大降低编译算法的编译效率。

编译效率同样是衡量知识编译算法的重要指标，因此为了保证编译效率和编译质量的双重提升，需要设计有效、快速的规约算法。本文通过研究DKCHER算法的执行流程以及编译结果发现，DKCHER算法中间结果EPCCL理论及最终编译结果EPCCL理论中存在大量满足规约规则的相邻子句。DKCHER算法在扩展子句的过程中使用互补展开，在保留扩展目标子句中所有文字的同时，通过逐渐递增变量的方式完成展开。因此相邻子句会包含较多的公共文字，会存在较多满足规约规则的相邻子句。

通过规约相邻子句能够有效减小目标EPCCL理论的规模。对于传统单阶段的EPCCL理论编译算法，如KCER、C2E等^{[11, 13]}，只能等编译过程完成之后才能使用规约算法约简编译结果EPCCL理论。因此，使用规约算法只能提升单阶段编译算法的编译质量，而不能提升其编译效率。而DKCHER算法采用双阶段的编译过程，若能在得到中间结果EPCCL理论后，对其进行有效地约简，降低第2阶段编译过程输入EPCCL理论的规模，则能够提高第2阶段编译过程的效率。若采用的规约算法效率较高，且约简效果较好，则能在提升DKCHER算法编译质量的同时提升其编译效率。

显然，仅约简满足规约规则的相邻子句的过程较约简所有满足规约规则的子句的过程精简许多，且通过分析，DKCHER算法的中间结果EPCCL理论和最终结果EPCCL理论中可能存在大量可规约的相邻子句。基于此本文设计了RACE算法，用于规约任意EPCCL理论中所有满足规约规则的相邻子句，该算法的执行流程如算法1所示。

算法1  RACE (reducing adjacent clauses in EPCCL)

输入  EPCCL理论E={D₁, D₂，…, D_h}；

输出  约简后的EPCCL理论。

1) 初始化: h=0, i=1

2) While h=0

3)   h=1

4)   While i < |E|

5)     If |C_i\\C_i+1|=1& |C_i|=|C_i+1|

6)       C=C_i\\C_i+1

7)       E=E\\{C_i, C_i+1}

8)       E=E∪{C}

9)       h=0

10) Return E

算法1中，用h控制规约所有满足规约规则的相邻子句。第5行中的判断条件用于判断C_i和C_i+1 2个相邻子句是否满足规约规则的条件，主要依据是：EPCCL理论中每对子句都包含互补文字对，说明任意2个子句的文字差集的模至少是1，因此，若EPCCL理论中任意2个子句长度相同且文字差集的模是1时，则这2个子句仅包含一对互补文字，且其他所有文字均相同，满足使用规约规则的条件^[13]。

结合RACE算法和DKCHER算法，本文设计了imp-DKCHER算法，该算法的执行流程如算法2所示。

算法2  imp-DKCHER

输入  令子句集F₁={C₁, C₂，…, C_n}, N包含了F中出现的所有变量；

输出  与F₁等价的EPCCL理论。

1) 初始化: F₂={□}, h=i=j=1

2) While i≤n

3)   F₁=F₁-{C}

4)   While j≤|F₂|

5)     If C与C_j互补Then skip

6)     Else If C|=C_j Then F₂=F₂-{C_j}

7)     Else C_j={C_j∨(C-Cj)}

8)     j++

9)   i++

10)   j=1

11) RACE(F₂)

12) If h=1 Then

13)   F₁=F₂

14)   h—

15)   Go to 3)

16) Else Return F₂

定理1   imp-DKCHER所得结果F₂等价于F，且F₂是一个EPCCL理论。

证明  由于DKCHER算法得到的结果等价于原子句集，并且是一个EPCCL理论，而本文提出的RACE算法仅作用于DKCHER单步计算结果EPCCL理论中的等价规约，并未改变DKCHER算法编译结果的等价性，因此定理1成立。

显然，使用RACE算法能够约简EPCCL理论的规模，而imp-DKCHER算法利用RACE算法将约简后的EPCCL理论作为第2阶段编译过程的输入，能够在一定程度上加速第2阶段的编译过程。因此，当imp-DKCHER算法第2阶段编译过程的加速时间大于中间结果EPCCL理论和编译结果EPCCL理论的规约时间之和时，imp-DKCHER算法的编译效率将优于DKCHER算法的编译效率。由于RACE算法具有较高的效率，因此结合上述分析可以合理地推测：大部分情况下，imp-DKCHER算法的编译效率会优于DKCHER算法的编译效率，该结论将在下一节通过实验得以验证。

3 实验结果与分析

本文在随机问题上的测试样例上对比测试了imp-DKCHER算法和DKCHER算法^[15]的编译效率和编译质量(主要使用EPCCL理论所包含的子句数来衡量)。本文实验平台如下：CPU：Intel(R) Core(TM) i5-6600 CPU @ 3.30 GHZ 3.31 GHZ，内存：8 GB，操作系统：Windows 10。

3.1 随机子句长度实例上的测试

本文参照文献[16]中采用的实验方法对比测试imp-DKCHER算法的编译效率和编译质量。首先，使用随机产生器随机生成子句长度不固定的测试样例，测试样例子句集中包含3个参数：变量个数n、子句个数m和最大子句长度k。n个变量对应2n个文字，在子句集生成过程中每个文字出现的概率是相同的，同时控制生成过程以避免生成重言式。

表 1给出了〈20, m, 10〉、〈25, m, 10〉和〈30, m, 10〉3种子句长度随机的测试样例上的对比测试结果，实验结果为50次实验的平均值。表 1中数据加框表示当前行最优编译质量，数据加粗和下划线表示当前行最优编译效率。下表类似, 恕不赘述。

从编译质量上看：对于子句长度随机的实例，imp-DKCHER算法始终能够提升DKCHER算法的编译质量，平均可提升15.9%左右。实验结果进一步验证了本文之前的分析结果，即DKCHER算法的中间结果EPCCL理论和最终结果EPCCL理论中包含较多的满足规约规则的相邻子句，而RACE算法能够规约所有满足规约规则的相邻子句，因此imp-DKCEHR算法的编译质量明显优于DKCHER算法。DKCHER算法是目前为止表现最好的EPCCL理论编译算法之一，尤其擅长子句数和变量数比值较大实例上的编译。本文提出的imp-DKCHER算法能够全面提升DKCHER算法的编译质量，不仅进一步扩大了DKCHER算法在子句数和变量数比值较大实例上的优势，同时弥补了DKCHER算法在子句数和变量数比值较小实例上的劣势。

从编译效率上看：对于子句长度随机的实例，imp-DKCHER算法在绝大部分实例上能够提升DKCHER算法的编译效率，仅在少部分实例上未能提升DKCHER算法的编译效率甚至有所下降，例如，在〈20, 100, 10〉的实例上，imp-DKCHER算法和DKCHER算法的编译效率相当，在〈25, 110, 10〉的实例上，imp-DKCHER算法的编译效率较差于DKCHER算法，但相差不大。之所以imp-DKCHER算法能够提升DKCHER算法的编译效率，主要是由于imp-DKCHER算法利用RACE算法降低了DKCHER算法中间结果EPCCL理论的规模。而在DKCEHR算第2步求差操作时，中间结果EPCCL理论将作为输入子句集完成与空子句的求差操作，因此中间结果规模的降低能够提高DKCHER算法第2步求差操作的效率。而RACE算法需要一定的时间寻找并规约满足规约规则的相邻子句。对于绝大多数子句长度随机的实例，RACE算法对于DKCHER算法第2步求差操作计算消耗的提升远大于其本身的运行时间，因此imp-DKCHER算法在绝大部分实例上能够显著提升DKCHER算法的编译效率。而对于小部分子句长度随机的实例，RACE算法对于DKCHER算法第2步求差操作计算效率的提升较小，然而其本身运行时间较短，因此imp-DKCHER算法的编译效率在小部分实例上与DKCHER算法相当或稍弱于DKCHER算法。

3.2 固定子句长度3-SAT实例上的测试

本文还用随机产生器生成了子句长度固定的3-SAT测试样例，即测试样例中的每个子句均包含3个文字。测试样例子句集中包含2个参数：变量个数n和子句个数m。

表 2给出了〈20, m〉、〈25, m〉和〈30, m〉3种随机3-SAT测试样例上的测试结果，实验结果同样为50次实验的平均值。

表 2进一步验证了表 1的结论。显然，imp-DKCHER算法在固定字句长度的实例上依旧能够显著提高DKCHER算法的编译质量，平均可提升18.6%。但相比于表 1，表 2中imp-DKCHER算法在较多的实例上未能提升DKCHER算法的编译效率，结合这些实例的实际情况会发现，当编译结果的规模较小时，imp-DKCHER算法的编译效率会低于DKCHER算法。主要原因在于：当编译结果规模较小时，意味着DKCHER算法中间结果EPCCL理论的规模较小，会导致使用RACE算法对DKCHER算法第2步求差操作的加速效果并不明显，甚至会低于规约中间结果EPCCL理论和最终结果EPCCL理论的总体运行消耗。

虽然在有些实例上，imp-DKCHER算法并未提升DKCHER算法的编译效率，然而相差并不大，例如，对于〈25, 107〉类型的实例，imp-DKCHER算法的编译效率相比于DKCHER算法仅相差2 ms，这主要得益于RACE算法的高效率。这也进一步说明了，RACE算法能够始终提升DKCHER算法的编译质量，且在大部分实例上，RACE算法能够同时提升DKCHER算法的编译效率，而在小部分实例上，RACE算法能够在保证DKCHER算法编译效率基本不变的同时提高其编译质量。

4 结论

1) 基于DKCHER算法得到的中间结果EPCCL论和最终结果EPCCL理论中存在大量可规约的相邻子句。

2) 本文提出的RACE算法能够约简EPCCL理论中所有满足规约规则的相邻子句，并基于此提升了DKCHER算法的编译质量和编译效率。

本文通过约简EPCCL理论中所有满足规约规则的相邻子句有效提升了DKCHER算法的性能，进一步扩大了扩展规则知识编译方法的应用范围。后续研究将利用规约规则提升其他扩展规则知识编译算法的性能，使扩展规则知识编译方法能够应用到更多相关领域问题的求解中。