软件学报  2017, Vol. 28 Issue (8): 2096-2112   PDF    
EPCCL理论的求交知识编译算法
牛当当1, 刘磊1, 吕帅1,2,3     
1. 吉林大学 计算机科学与技术学院, 吉林 长春 130012;
2. 吉林大学 数学学院, 吉林 长春 130012;
3. 符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012
摘要: 超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以EPCCL(each pair of clauses contains complementary literals)理论的形式保存.基于超扩展规则的性质,提出一种EPCCL理论编译算法:求交知识编译算法IKCHER(intersection approach to knowledge compilation based on hyper extension rule).该算法适合难解类SAT问题的知识编译,也是一种可并行的知识编译算法.研究了如何实现多个EPCCL理论的求交操作,证明了EPCCL理论的求交过程是可并行执行的,并设计了相应的并行求交算法PIAE(parellel intersection of any number of EPCCL).通过对输入EPCCL理论对应普通子句集的利用,设计了一种高效的并行求交算法imp-PIAE(improvement of PIAE).基于上述算法,还设计了两种并行知识编译算法P-IKCHER(IKCHER with PIAE)和impP-IKCHER(IKCHER with imp-PIAE),分别采用PIAE并行合并算法和imp-PUAE并行合并算法.最后,通过实验验证了,大部分情况下,IKCHER算法的编译质量是目前为止所有EPCCL理论编译器中最优的,P-IKCHER算法所使用的合并策略并没有起到加速的效果,反而使得编译效率和编译质量有所下降;impP-IKCHER算法提高了IKCHER算法的编译效率,CPU四核环境下最高可提高2倍.
关键词: 知识编译     扩展规则     超扩展规则     EPCCL(each pair of clauses contains complementary literals)理论     并行知识编译    
Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories
NIU Dang-Dang1, LIU Lei1, LÜ Shuai1,2,3     
1. College of Computer Science and Technology, Jilin University, Changchun 130012, China;
2. College of Mathematics, Jilin University, Changchun 130012, China;
3. Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China
Foundation item: National Natural Science Foundation of China (61300049, 61502197, 61503044); Specialized Research Fund for the Doctoral Program of Higher Education of China (20120061120059); Key Program for Science and Technology Development of Jilin Province of China (20130206052GX); Natural Science Research Foundation of Jilin Province of China (20140520069JH, 20150101054 JC, 20150520058JH)
Abstract: HER (hyper extension rule) is an expansion of ER (extension rule). The results of computing the union and difference set of two sets of maximum terms which are extended by two clauses respectively based on the hyper extension rule can be saved as EPCCL (each pair of clauses contains complementary literals) theories. In this paper, a parallelizable knowledge compilation algorithm for EPCCL theories, IKCHER, is proposed based on computing the intersection of maximum terms sets. The focus is placed on the research of parallel computing the intersection sets of multiple EPCCL theories based on HER, resulting in the design of the corresponding algorithm, PIAE (parallel intersection of any number of EPCCL). Through using the origin CNF formulae of EPCCL theories, another efficient merging algorithm imp-PIAE is proposed. Based on above methods two parallel knowledge compilation algorithms P-IKCHER and impP-IKCHER are constructed for EPCCL theories, utilizing the PIAE algorithm and imp-PIAE algorithm to merge multiple EPCCL theories respectively. Experimental results show that IKCHER algorithm has the best compilation quality of all EPCCL compilation algorithms. P-IKCHER algorithm does not improve the compilation quality and compilation efficiency of IKCHER while impP-IKCHER algorithms can maintain the compilation quality of IKCHER, and improve the compilation efficiency of IKCHER. When the number of CPU cores is 4, the compilation efficiency of IKCHER can be improved twice as much in the best cases.
Key words: knowledge compilation     extension rule     hyper extension rule     EPCCL (each pair of clauses contains complementary literals) theory     parallel knowledge compilation    

可满足性问题(SAT问题)是NP完全问题的核心[1], 相变现象在不同形式的SAT问题中是普遍存在的[2, 3], 相变点附近的命题可满足性判定通常需要巨大的时间开销.目前, 主要通过改善局部搜索或设计新型启发式等手段使SAT求解得以高效实现[4-8].SAT求解并行化是提高SAT求解效率的重要手段之一, 同时也是一个热门领域[9-11].知识库的查询操作通常是通过调用SAT求解器完成的, 然而SAT求解始终需要指数级的时间, 因此, 通过多次调用SAT求解器完成对同一个知识库的多次查询显然是不合适的.

知识编译的主要目的是为了提高重复性任务的计算效率, 主要思想为, 将问题的求解分为两个基本阶段:离线编译和在线推理.Val给出了可控制类的概念, 可以作为目标编译语言的判断标准[12].Van den Broeck等人研究了约简的SDD(sentential decision diagram)语言上多项式时间内的推理方法[13].Marquis和Fargier等人研究了几种不同目标编译语言中存在的闭包[14, 15].Darwiche提出了一种将子句形式的命题公式编译为可分解否定范式(DNNF)的完备知识编译方法[16, 17], 并给出了知识编译图谱[18].Fargier基于Krom, Horn和Affine这3种较有影响力的命题片段对Darwiche提出的知识编译图谱做了扩充[19], 并设计了针对变种表示语言的知识编译图谱[20]和有序真值决策图的知识编译图谱[21].Koriche等人研究了基于Affine决策树的模型计数方法, 并弥补了知识编译图谱中Affine族的空缺[22].Lai等人设计了带有蕴含文字的有序二元决策图, 是一种新的知识编译语言[23].目前, 国际上针对知识编译的研究大多集中于对各种知识编译语言的比较以及如何提高目标语言的查询能力上.知识编译方法与SAT求解存在着紧密的联系, 例如, 可满足判定是知识编译图谱中8种查询操作的一种[18]; Huang等人基于先进的SAT求解器实现了多种知识编译语言的编译[24].因此, 如何借鉴并行SAT求解的方法实现知识编译方法的并行化, 也是一个值得探索的新领域.

2003年, Lin等人提出了扩展规则推理方法(extension rule, 简称ER)[25], 被著名人工智能专家Davis称为与归结方法“互补”的方法.与归结方法相反, 扩展规则推理方法通过扩展出所有极大项组成的集合判定子句集的可满足性.Lin等人基于扩展规则提出了一种新的命题逻辑理论证明方法IER[25].殷明浩等人提出了CER算法.该算法基于容斥原理解决了ER算法在求解#SAT问题的空间复杂性问题[26].赖永等人提出了一种命题扩展规则方法ER的高效实现和#ER算法, 并结合#DPLL算法和#ER算法提出了#CDE算法, 具有较高的命题推理效率和#SAT求解效率[27].李莹等人在ER算法的基础上提出了分别基于IMOM和IBOHM启发式策略的IMOMH_ IER和IBOHMH_IER算法, 提高了扩展规则推理算法的效率[28].此外, 李莹等人基于扩展规则还提出了一种新的定理证明技术NER[29].在扩展规则的基础上, Lin等人提出了一种基于扩展规则的知识编译方法KCER, 可以将子句集编译为EPCCL理论[30].EPCCL理论是一种高效的目标编译语言, 相对于现有知识编译语言具有较强的竞争力, 基于EPCCL理论能够在线性时间内实现知识编译图谱中的全部查询操作.因此, 深入研究EPCCL理论的特性, 通过挖掘EPCCL编译器编译过程中的有效信息来提高编译效率及编译质量, 对于EPCCL理论的发展具有重要意义.Yin等人基于扩展规则和知识编译设计了求解模型计数问题的KCCER算法.该算法具有较高的效率[26, 31].谷文祥等人设计了MCN和MO两种启发式策略, 提高了KCER算法的编译效率, 并降低了编译后的子句集规模[32].刘大有等人基于扩展规则提出了一种新的EPCCL理论编译器C2E.该编译器有较高的编译效率[33].我们基于超扩展规则[34]提出了扩展反驳的概念, 在扩展反驳与知识编译之间建立了联系, 并提出了两种知识编译算法:DKCHER和UKCHER[35].目前为止, 与其他EPCCL理论编译算法相比, DKCHER对于相变点附近的难解问题有非常优秀的编译效率和编译质量, 且对于子句数和变量数的比值较大的子句集同样能够取得最优的编译效率和编译质量, 是目前为止最优秀的EPCCL理论编译算法, 然而它并不能直接并行化.通过分析算法UKCHER的执行过程, 证明了它是目前为止唯一一个能够并行知识编译的EPCCL理论编译算法, 然而其编译质量和编译效率较差.因此, 对于EPCCL理论编译算法的提升, 存在两种主要途径:(1) 提高串行编译算法的编译质量和编译效率; (2) 将优秀的EPCCL理论编译算法并行化.

本文基于我们提出的超扩展规则[34], 设计了一种新的EPCCL理论编译算法IKCHER.同时, 本文还设计了两种并行求交策略PIAE和imp-PIAE, 均能求得任意两种EPCCL理论所能扩展出的极大项集的交集.基于上述两种并行求交策略, 本文设计了两种并行EPCCL理论编译算法:P-IKCHER和impP-IKCHER.实验结果表明:大部分情况下, IKCHER算法的编译质量是目前为止所有EPCCL理论编译器中最优的, 其求解效率与目前最好的EPCCL理论编译器DKCHER算法相当; P-IKCHER算法所使用的合并策略并没有起到加速的效果, 反而使得编译效率和编译质量有所下降; impP-IKCHER算法提高了IKCHER算法的编译效率, 四核并行下最高可提高2倍.目前, 尚未出现关于并行知识编译的成果, 本文的研究工作能够为其他EPCCL理论编译算法的并行化及其他目标语言编译算法的并行化提供借鉴.

本文第1节介绍超扩展规则的基本概念和性质.第2节介绍求交知识编译算法IKCHER.第3节对本文提出的IKCHER算法与DKCHER、C2E等优秀EPCCL理论编译算法做对比测试.第4节设计两种并行求交策略PIAE和imp-PIAE, 并提出两种对应的EPCCL理论并行知识编译算法P-IKCHER和impP-IKCHER.第5节测试两种EPCCL理论并行知识编译算法的编译质量和编译效率.最后为本文总结.

1 超扩展规则

扩展规则能够对单个子句和单个原子进行扩展操作.在求解推理问题的过程中, 直接对多个子句操作能够提高处理效率, 并且尽可能多地利用潜在的问题结构.超扩展规则可应用于两个子句, 是经典扩展规则的扩展形式.

定义1(扩展规则(extension rule))[25].给定一个子句C和一个变量集M, D={Ca, C∨¬a}, 其中aM并且a和¬a都不在C中出现, 将CD的推导过程称为扩展规则, D中的子句称为C扩展得到的结果, 并且CD.

由定义1可以看出, 扩展规则与归结规则是完全相反的规则.同时, 定义1应用扩展规则后得到的子句集与原子句集等价.因此, 扩展规则可以被看作是一条新的推理规则.应用扩展规则后, D中子句间存在互补文字对.应用扩展规则推理方法过程中, 期望得到扩展结果中子句间最好存在更多的互补文字对, 以利用扩展规则的推理特性:依赖扩展规则的推理方法适用于互补因子较高的子句集可满足性判定[15].

根据文献[25], 称任意一个子句C为变量集M上的极大项, 当且仅当C包含|M|个M中互不相同的变量.扩展规则要求一个子句针对一个变量进行扩展, 超扩展规则允许一个子句针对另一个子句进行扩展.为了表示方便, 定义子句C的(原子)变量集合为V(C), 子句C关于变量集M所能扩展出的极大项集合为JM(C), 子句集F的(原子)变量集合为V(F).本文所研究的子句集中不包含重言式, 同时符号“≡”表示式子两边语义等价.对于单个子句C, CJM(C).

定义2(超扩展规则(hyper extension rule)).给定两个子句CA, D={CA, C∨¬A}, 其中, V(C)∩V(A)=∅, 将CD的推导过程称为超扩展规则, D中的元素为C应用超扩展规则的结果.

本文为了表示更直观, 在定义2中规定V(C)∩V(A)=∅, 然而该条件并非必要条件.由定义2可以推出:如果A$\nvDash$C, 且AC不包含互补文字对, 则利用AC扩展所得到的结果为D={CA, C∨¬(V(A)-V(C))}, 其中, CA为标准子句, 即不包含相同的文字.超扩展规则中, 子句C与其应用超扩展规则的扩展结果D是等价的.

与经典扩展规则不同, 超扩展规则用子句A对子句C进行扩展, 但这种扩展方法产生的C∨¬A为非子句形式(CA为标准子句形式), 因此需要对C∨¬A以适当形式展开.假设A={l1, …, ln}, 则运用De Morgan律.

$ E=\{C\vee \neg A\}=\{C\vee \neg ({{l}_{1}}\vee \ldots \vee {{l}_{n}})\}=\{C\vee \neg {{l}_{1}}, \ldots, C\vee \neg {{l}_{n}}\}. $

上述展开过程是语义等价的, 但由于每个li(i=1, …, n)两两不同且均不在C中出现, 所以E的互补因子较低, 难以利用扩展规则的推理特性.为了保证扩展结果子句间的互补性, 采用如下方法展开:

$ \begin{align} & \underline{ \neg ({{l}_{1}}\vee ...\vee {{l}_{n}}) } \\ & (\neg {{l}_{1}}) \\ & ({{l}_{1}}\vee \neg {{l}_{2}}) \\ & ... \\ & ({{l}_{1}}\vee ...\vee {{l}_{n-1}}\vee \neg {{l}_{n}}) \\ \end{align} $ (1)

公式(1) 的展开过程称为互补展开, 则E={C∨¬A}={C∨¬l1, Cl1∨¬l2, …, Cl1∨…∨ln-1∨¬ln}, 进而,

$ D=\{C\vee {{l}_{1}}\vee \ldots \vee {{l}_{n}}, C\vee \neg {{l}_{1}}, C\vee {{l}_{1}}\vee \neg {{l}_{2}}, \ldots, C\vee {{l}_{1}}\vee \ldots \vee {{l}_{n}}_{-1}\vee \neg {{l}_{n}}\}. $

依赖公式(1) 的互补展开保证了超扩展规则的等价性, 并且展开结果中子句之间存在互补文字对.同样, 也可以采用公式(2) 的形式描述互补展开:

$ CN{{F}_{linear}}(A\vee \neg (l\vee B))=\left\{ \begin{array}{*{35}{l}} A\vee \neg l, \text{ }|B|=0 \\ \{A\vee B\vee \neg l\}\cup CN{{F}_{linear}}(A\vee \neg B), \text{ }|B|>0 \\ \end{array} \right. $ (2)

定义3(EPCCL理论)[30].若子句集F是一个EPCCL理论, 则F中任意两个子句间均含有互补文字对.

超扩展规则能够利用一个子句扩展另一个子句, 并且利用互补展开在保证可满足性等价的前提下保证了扩展之后的子句间存在互补文字对, 这使得扩展过程能够高效进行并得到能够发挥扩展规则推理方法特性的理论.

超扩展规则还具有以下特殊性质[35].

性质1[35].对两个子句使用超扩展规则得到的结果是一个EPCCL理论, 由于互补展开使得超扩展规则的展开结果中所有子句之间存在互补文字对, 因此使用超扩展规则得到的结果是一个EPCCL理论.

性质2[35].基于超扩展规则可以计算任意两个子句所能扩展出的极大项的交集.

对于两个子句CA, 如果A$\nvDash$C, 且AC不包含互补文字对, 则利用子句A扩展子句C可以得到结果D={CA, C∨¬(V(A)-V(C))}, 其中, CA代表了JM(C)∩JM(A).

性质3[35].基于超扩展规则能够利用EPCCL理论保存两个子句所能扩展的极大项集的差集.

对于两个子句CA, 如果A$\nvDash$C, 且AC不包含互补文字对, 则利用子句A扩展子句C可以得到结果D={CA, C∨¬(V(A)-V(C))}, 其中, {C∨¬(V(A)-V(C))}代表了JM(C)-JM(A).

2 基于超扩展规则的求交知识编译算法

在文献[35]中, 我们利用超扩展规则的性质1和性质3设计了求并知识编译算法UKCHER和求差知识编译算法DKCHER, 其中, DKCHER算法是目前为止最优秀的EPCCL理论编译算法, UKCHER算法是目前为止唯一可并行的EPCCL理论编译算法.本节我们将利用超扩展规则的性质2设计一种新的可并行知识编译算法IKCHER.IKCHER算法采用了与DKCHER算法类似但不同的求解结构.该算法继承了DKCHER算法的优秀特性, 并且还具备了可并行的新特性.

根据文献[35], 子句□在变量集M(|M|=2m)上所能扩展出的极大项集为M上所有极大项的全集, 令H表示等价于子句集FM上所不能扩展出的极大项集的子句集, 则JM(H)=JM(□)-JM(F)且JM(F)=JM(□)-JM(H).若利用超扩展规则能够求得JM(H), 且将JM(H)保存为一个EPCCL理论, 就能利用JM(H)求得JM(F), 且所得结果仍然是一个EPCCL理论.基于上述过程, 能够将任意子句集编译为与之等价的EPCCL理论.为了求得任意子句集所不能扩展出的极大项集, 本文利用定理1对求解过程进行具体描述.

定理1.给定子句集F={C1, …, Cn}, M为在F中出现的所有变量的集合, 令H为等价于F所不能扩展出的极大项集的子句集, 则JM(H)=JM(□)-JM(F)=JM(□)-JM(C1)-…-JM(Cn)=$\bigcap\limits_{1\le i\le n}{({{J}_{M}}(\square )-{{J}_{M}}({{C}_{i}}))}.$

证明:由于JM(F)=$\bigcup\limits_{1\le i\le n}{{{J}_{M}}({{C}_{i}})}$, 因此定理1显然成立.

定理1中, 根据超扩展规则性质3可求得任意JM(□)-JM(Ci)(1≤in), 且所得结果为一个EPCCL理论.假设Ci=l1∨...∨lk, 则JM(□)-JM(Ci)≡{¬l1, l1∨¬l2, …, l1∨…∨lk-1∨¬lk}, 显然, 等式右边为一个EPCCL理论.

将所有的JM(□)-JM(Ci)求解为EPCCL理论后, 再求$\bigcap\limits_{1\le i\le n}{({{J}_{M}}(\square )-{{J}_{M}}({{C}_{i}}))}$, 并需要保证所得结果仍然是一个

EPCCL理论.为此, 我们首先提出了定理2.

定理2.给定两个EPCCL理论E1={R1, …, Rp}和E2={T1, …, Tq}, 则E1E2M上所能扩展出的极大项集的交集S=JM(E1)∩JM(E2)≡{I1, …, Ipxq}, 其中, 任意Ii(1≤ipxq)为JM(R(i-1)/q+1)∩JM(T(i-1) mod q+1)的计算结果, 且S为一个EPCCL理论.

证明:由于${{J}_{M}}({{E}_{1}})=\bigcup\limits_{1\le i\le p}{{{J}_{M}}({{R}_{i}})}{{J}_{M}}({{E}_{2}})=\bigcup\limits_{1\le j\le q}{{{J}_{M}}({{T}_{j}})}$, 因此,

$ {{J}_{M}}({{E}_{1}})\cap {{J}_{M}}({{E}_{2}})=\bigcup\limits_{1\le i\le p}{{{J}_{M}}({{R}_{i}})}\cap \bigcup\limits_{1\le j\le q}{{{J}_{M}}({{T}_{j}})}=\bigcup\limits_{1\le i\le p, 1\le j\le q}{({{J}_{M}}({{R}_{i}})\cap {{J}_{M}}({{T}_{j}}))}; $

由于任意IiJM(R(i-1)/q+1)∩JM(T(i-1) mod q+1)(1≤ipxq), 因此, {I1, …, Ipxq}≡$\bigcup\limits_{1\le i\le p, 1\le j\le q}{({{J}_{M}}({{R}_{i}})\cap {{J}_{M}}({{T}_{j}}))}.$

定理2成立.

定理2中需要计算任意两个子句所能扩展出的极大项, 利用超扩展规则性质2能够求得两个非互补且不存在蕴含关系的子句的所能扩展出的极大项集的交集.对于两个互补或存在蕴含关系的子句, 需要单独考虑其所能扩展出极大项集交集的求解.

引理1[35].如果两个子句CiCj包含互补文字对, 则其在M上所能扩展出的极大项集的交集JM(Ci)∩ JM(Cj)=∅.

根据引理1, 能够计算互补子句的所能扩展出的极大项集的交集, 对于非互补的子句, 本文采用定理3的方式进行计算.

定理3.若两个子句Ci=l1∨...∨lkCj=g1∨...∨gh不包含互补文字对, 则其在M上所能扩展出的极大项集的交集JM(Ci)∩JM(Cj)=b1∨...∨bs, 其中, {b1, ..., bs}={l1, ..., lk}∪{g1, ..., gh}.

证明:子句Ci所能扩展出的极大项集中, 所有极大项必然包含文字集{l1, ..., lk}; 子句Cj所能扩展出的极大项集中, 所有极大项必然包含文字集{g1, ..., gh}.因此, JM(Ci)∩JM(Cj)中所有极大项必然包含文字集{l1, ..., lk}∪ {g1, ..., gh}, 从而定理3成立.

根据引理1和定理3, 能够求得任意两个子句所能扩展出的极大项集的交集, 因此能够将定理2中任意Ii (1≤ipxq)用子句的形式表示.

定理4.利用引理1和定理3对定理2中任意Ii(1≤ipxq)进行求解, 所得结果{I1, …, Ipxq}仍为一个EPCCL理论.

证明:根据引理1和定理3, 所得结果{I1, …, Ipxq}中会存在若干恒真子句, 可以直接忽略.剩余子句中, 任取两个子句IxIy, 假设Ix是由CiCj求极大项交集而得(CiE1 & CjE2), Iy是由CgCh求极大项交集而得(CgE1 & ChE2), 显然, CiCg之间存在互补文字对, CjCh之间存在互补文字对.根据定理3, Ix子句由CiCj中所包含文字的并集组成, IyCgCh中所包含文字的并集组成, 因此, IxIy之间必然存在互补文字对.综上, {I1, …, Ipxq}是一个EPCCL理论, 定理4成立.

根据上述定理, 能够求得任意两个EPCCL理论所能扩展出的极大项集的交集, 所得结果仍为EPCCL理论.因此, 对于任意子句集F={C1, …, Cn}, 首先求出每个子句Ci所不能扩展出的极大项集, 并用EPCCL理论Ei予以保存, 然后利用定理2逐步求出H=E1∩…∩En, 所得结果H等价于F所不能扩展出的极大项集.再用相同过程求得H所不能扩展出的极大项集, 并用EPCCL理论保存, 该EPCCL理论等价于F.本文将上述过程具体化为算法形式, 并将该算法称为IKCHER, 描述如下.

算法1. IKCHER.

1.输入:令子句集F1={C1, …, Cn}, M包含了F中出现的所有变量.

2. h=1

3.初始化:F2={¬C1}, F3=∅, i=2, j=k=1

4. While i≤|F1|

5.   Si={¬Ci的互补展开} //JM(□)-JM(Ci), 变量集M包含了F中出现的所有变量

6.   While j≤|F2|

7.     If CiCj互补Then skip

8.     Else

9.       While k≤|Ci|

10.         If Si[k]与Cj互补Then skip

11.         Else if Si[kCj Then F3=F3∪{Cj}

12.         Else if Cj‘Si[k] Then F3=F3∪{Si[k]}

13.         Else F3=F3∪{Cj∨(Si[k]-Cj)}

14.         k++

15.     j++

16.     k=1

17.   F2=F3

18.   F3=∅

19.   i++

20.   j=1

21. If h=1 Then

22.   F1=F2

23.   h--

24.   Goto 3

25. Else return F2

定理5. IKCHER算法是正确完备的, 且输出结果是一个等价的EPCCL理论.

证明:利用超扩展规则的性质3, IKCHER算法中的第5行实现了□与F中第i个子句Ci所能扩展出的极大项集的差集, 计算结果为一个EPCCL理论.第4行中的循环保证了能够求得所有JM(□)-JM(Ci)(1≤in), 第6行的循环用于计算前i-1个子句所不能扩展出的极大项集与第i个子句所不能扩展出的极大项集的交集, 所得结果即为前i个子句所不能扩展出的极大项集.根据定理4, F2始终是EPCCL理论, 因此, 当第4行的循环结束后就能求得与F1所不能扩展出的极大项集等价的EPCCL理论F2.算法在第21行控制利用h继续求解F2所不能扩展出的极大项集, 再次求解所得结果即为与F1等价的EPCCL理论.因此, IKCHER算法是正确而完备的.

通常情况下, SAT问题的难解程度与其解的个数具有直接关系, 难度越大则解越少.将问题编译为等价的EPCCL理论之后, 编译结果所能扩展出的极大项数与弄假原子句集解的个数是相等的, 因此直观上看, 对于难解类SAT问题, 直接将其编译为等价的EPCCL理论, 其结果的规模将是非常庞大的.在编译难解类SAT问题时, 与DKCHER算法类似, IKCHER算法采用两阶段式的编译:第1阶段所得结果为原子句集所不能扩展出的极大项集, 该集合的模与原子句集的模型数是等价的, 且该结果为一个EPCCL理论, 因此, 第1阶段所得结果的规模将会是非常小的; 第2阶段将求得第1阶段所得结果所不能扩展出的极大项集, 并将结果保存为一个EPCCL理论, 由于第1阶段所得结果的规模较小以及互补展开的特性, 编译结果中会存在较多短子句, 这些短子句甚至短于原子句集中任意子句, 因此, 第2阶段所得结果的规模将远远小于直接编译所得结果的规模.因此理论上, IKCHER算法对于求解难度较大的SAT问题具有较好的编译效果.

另外, IKCHER算法求解过程中会利用互补展开求解每个子句所不能扩展出的极大项集, 并在展开后的EPCCL理论上进行求交操作, 而DKCHER算法每次对一个子句进行求差操作, 因此, IKCHER算法求解过程比DKCHER算法求解过程所能获得的启发式信息更多, 依据这些启发式信息所设计的启发式策略也将更加直观、高效.

3 IKCCER算法编译效果的对比测试

本文提出了一种新的EPCCL理论编译算法:IKCHER算法.KCER算法[30]、C2E算法[33]、UKCHER算法[35]和DKCHER算法[35]均能将任意子句集编译为等价的EPCCL理论, 其中, DKCHER算法是目前为止表现最好的EPCCL理论编译器.本文在随机问题和国际上通用的测试用例上对比测试了IKCHER算法的编译效率和编译质量(使用编译结果中子句数量进行衡量).本文实验平台如下:

● CPU:Intel Core(TM) i7-3770 CPU@3.40GHZ 3.40GHZ;

● 内存:8GB;

● 操作系统:Windows 10.

3.1 对于随机子句长度的子句集上IKCHER算法的测试

我们用随机产生器生成了子句长度不固定的测试样例, 随机产生器的结果为包含3个参数〈m, n, k〉的子句集, 其中, m为变量个数, n为子句个数, k为每个子句的最大长度.本文提出的知识编译算法和现有的EPCCL理论编译算法均不支持大规模的实例, 表 1~表 3中分别给出了〈20, n, 10〉, 〈25, n, 10〉和〈30, n, 10〉这3种变量数固定、子句数不同的随机测试样例的编译结果, 实验结果为50次实验的平均值, size表示子句个数, time表示运行时间(单位为s), □表示相应算法编译质量最优.下表类似, 不再赘述.

Table 1 Experimental results on random instances 〈20, n, 10〉 表 1 随机实例〈20, n, 10〉的实验结果

Table 2 Experimental results on random instances 〈25, n, 10〉 表 2 随机实例〈25, n, 10〉的实验结果

Table 3 Experimental results on random instances 〈30, n, 10〉 表 3 随机实例〈30, n, 10〉的实验结果

基于表 1~表 3能够观察出以下现象:(1) 当变量数固定时, IKCHER算法和DKCHER算法的编译结果的规模和编译所需时间会随着子句数的增加而减少; (2) 当子句集规模较小时, UKCHER算法、C2E算法和KCER算法的编译结果的规模和编译所需时间随着子句数的增加而增加; (3) 当子句集规模大于某一临界值时, UKCHER算法、C2E算法和KCER算法的编译结果的规模会维持不变, 甚至减少; (4) 由于样例随机生成, 因此可能会存在少量的波动.例如表 2中, 当n < 90时, UKCHER算法、C2E算法和KCER算法的编译结果的规模和编译所需时间随着子句数的增加而逐渐增加(现象(2)); 当n≥90时, UKCHER算法、C2E算法和KCER算法的编译所需时间仍然随着子句数的增加而逐渐增加, 其编译结果的规模却逐渐稳定下来(现象(3)); 当n≥90时, UKCHER算法、C2E算法和KCER算法编译结果的规模均上下无规律波动(现象(4)).类似的现象同样出现在表 1表 3中.

从编译规模来看, 表 1~表 3中, 45.8%的实例下, IKCHER算法的编译质量是最优的; 41.7%的实例下, DKCHER算法的编译质量是最优的; 12.5%的实例下, C2E的编译质量是最优的.由于DKCHER算法和IKCHER算法的编译质量的差值较小, 因此可以认定IKCHER算法和DKCHER算法的编译质量相当, 二者在大多数情况下是最优的.表 1中, 当n < 90时, C2E算法的编译规模会随着子句数的增加而增加; 当n≥90时, C2E算法的编译规模会稳定在2 100左右.同样的现象出现在KCER算法中, 不过整体来看, KCER算法的编译规模大于C2E算法的编译规模.表 1中, 当n < 50时, IKCHER算法和DKCHER算法的编译规模大于C2E算法的编译规模; 然而随着子句数的增加, 当n≥50时, IKCHER算法和DKCHER算法的编译规模远远小于C2E和KCER的编译规模.甚至当n=100时, C2E算法的编译规模是IKCHER算法的107倍, 是DKCHER算法编译规模的128倍; KCER算法编译规模是IKCHER算法的193倍, 是DKCHER算法编译规模的254倍.由此可知, 求交知识编译算法IKCHER对于变量数固定、子句数规模较大的子句集能够取得很好的编译效果.UKCHER算法的编译规模始终大于C2E算法的编译规模, 而和KCER算法的编译规模接近, 但是小于后者.从表 2表 3可以得到和表 1相同的结论.

从编译效率来看, 表 1中, 当n≤50时, UKCHER算法的效率是最高的, C2E算法居于第3位, 而IKCHER算法和DKCHER算法的效率最差.这是由于IKCHER算法和DKCHER算法的扩展过程中都需要保存较多的中间结果, 其中很多无效的中间结果会参与到算法扩展过程中, 影响了整体执行效率.当n > 50时, DKCHER算法的编译效率最高, IKCHER算法的编译效率排在第2位, 但是与DKCHER算法的编译效率相差不大; 同时, 随着子句数的增加, UKCHER算法和KCER算法所需编译时间也随之大幅度增加, 二者的编译效率最终均差于C2E算法.表 3中, IKCHER算法的编译效率始终差于C2E算法的编译效率.整体来看, 对于随机长度的SAT问题, IKCHER算法适用于变量数较小、子句数较大的子句集.

3.2 对于标准3-SAT子句集上IKCHER算法的测试

为了更全面地展示本文提出的知识编译算法的特性, 本文还随机生成了变量数固定、子句数改变的标准3-SAT子句集, 表 4~表 6分别给出了〈20, n〉, 〈25, n〉和〈30, n〉这3种不同3-SAT子句集实例的样例进行测试, 测试结果为50次实验的平均值.

Table 4 Experimental results on random 3-SAT instances 〈20, n 表 4 随机3-SAT实例〈20, n〉的实验结果

Table 5 Experimental results on random 3-SAT instances 〈25, n 表 5 随机3-SAT实例〈25, n〉的实验结果

Table 6 Experimental results on random 3-SAT instances 〈30, n 表 6 随机3-SAT实例〈30, n〉的实验结果

基于表 4~表 6能够得出:(1) 对于3-SAT子句集, 当变量数固定、子句数改变时, UKCHER、C2E和KCER这3种知识编译算法的编译规模均随着变量数的增加而增加; (2) IKCHER算法和DKCHER算法的编译规模会随着子句数的增加而减少, 而二者的编译质量相差不大.然而, 其中62.5%的实例下, IKCHER算法的编译质量是最优的; 37.5%的实例下, DKCHER算法的编译质量是最优的, 因此从编译质量角度考虑, 在编译3-SAT子句集时, 应尽可能地选择IKCHER算法.从编译效率上来看, DKCHER算法的编译效率在大多数情况下优于IKCHER算法的编译效率, 但是二者相差不大.

表 6中, 由于变量数过大, UKCHER算法和KCER算法会经常内存溢出, 因此, 对于表 6中的很多实例, UKCHER和KCER是无法解决的.显然, 二者不适用于变量数较多的3-SAT问题.

为了验证IKCHER算法并行化的可行性, 本文进一步研究了如何实现IKCHER算法的并行化.

4 求交知识编译算法的并行化

本文将求解多个EPCCL理论所能扩展出的极大项集简称为EPCCL理论求交, EPCCL理论求交对于实现IKCHER算法的并行化是一个关键问题.

4.1 EPCCL理论的求交操作

事实上, IKCHER算法中用到了两个EPCCL理论的求交操作, 算法执行过程中需要不断地对F2Si进行求交操作.定理2给出了两个EPCCL理论求交的具体过程, 任意两个EPCCL理论E1={R1, …, Rp}和E2={T1, …, Tq}求交之后, 所得结果为一个EPCCL理论:S=JM(E1)∩JM(E2)≡{I1, …, Ipxq}, 其中, 任意Ii(1≤ipxq)为JM(R(i-1)/q+1)∩ JM(T(i-1) mod q+1)的计算结果.显然, 上述过程可以并行分解, 由于任意IiIj的求解过程之间互不影响, 因此可以并行求解{I1, …, Ipxq}.我们可以将E1拆分成k个子集$E_{1}^{1}, ..., E_{1}^{k}$, 然后并行求得$\bigcup\limits_{1\le i\le k}{(E_{1}^{i}\cap {{E}_{2}})}$, 所得结果即为E1E2所能扩展出的极大项集的交集.

由于两个EPCCL理论求交之后仍然是一个EPCCL理论, 因此可以采用增量式的思想并行求得任意多个EPCCL理论所能扩展出的极大项集的交集.根据上述过程, 我们设计了多个EPCCL理论的并行求交算法, 并称其为PIAE.该算法描述如下.

算法2. PIAE.

1.输入:s个EPCCL理论{E1, …, Es}

2. E=E1, h=2

3. While hs

4.   Divide Eh to $\{E_{h}^{1}, ..., E_{h}^{k}\}$

5.   Parallel

6.   Foreach $E_{h}^{v}$ (1≤vk)

7.     d=1

8.     While d≤|$E_{h}^{v}$|

9.       Tv=ICE(E, Cd) (CdEhv)

10.       d++

11.     End parallel

12.     E=T1∪…∪Tk

13.     h++

14. Return E

Sub-procedure ICE (CNF F={C1, …, Cn}, clause C)

1.令F1=∅, i=j=1

2. While i≤|F|

3.     If CCi互补Then skip

4.     Else if C‘Ci Then F1=F1∪{Ci}

5.     Else if Ci‘C Then F1=F1∪{C}

6.     Else F1=F1∪{Ci∨(C-Ci)}

7.     j++

8.   j=1

9.   i++

10. Return F1

算法2实现了k个EPCCL理论进行的并行求交操作, 并将结果保存为EPCCL理论.该算法利用第3行的while循环实现EPCCL理论的增量式求交操作; 在第4行, 将已合并的EPCCL理论分为k份, 然后和下一个未操作的EPCCL理论进行并行求交操作; 第5行~第11行是算法的并行操作部分; 第12行将求交结果合并.该算法在第9行调用了子程序ICE.ICE的功能是求解一个子句与一个子句集所能扩展出的极大项集的交集, 若输入子句集是一个EPCCL理论, 则输出的子句集为EPCCL理论, 否则为普通子句集.

定理6.给定一个EPCCL理论E={R1, …, Rp}和一个子句集F={T1, …, Tq}, 则E1FM上所能扩展出的极大项集的差集$S={{J}_{M}}(E)-{{J}_{M}}(F)\equiv \bigcup\limits_{1\le i\le p}{({{J}_{M}}({{R}_{i}})\cap {{J}_{M}}(\neg {{T}_{1}})\cap ...\cap {{J}_{M}}(\neg {{T}_{q}}))}$, 且S为一个EPCCL理论.

证明:根据定理1, JMT1)∩…∩JMTq)能够表示F所不能扩展出的极大项集,

则任意JM(Ri)∩JMT1)∩…∩ JMTq)能够表示RiFM上所能扩展出的极大项集的差集,

因此, $S={{J}_{M}}(E)-{{J}_{M}}(F)\equiv \bigcup\limits_{1\le i\le p}{({{J}_{M}}({{R}_{i}})\cap {{J}_{M}}(\neg {{T}_{1}})\cap ...\cap {{J}_{M}}(\neg {{T}_{q}}))}$成立.

又由于JM(Ri)∩JMT1)∩…∩JMTq) JM(Ri)且E={R1, …, Rp}是一个EPCCL理论,

因此, S是一个EPCCL理论.

根据定理6, PIAE算法中, 若能知道输入EPCCL理论对应与其所不能扩展出的极大项集等价的普通子句集, 则可以直接对普通子句集操作.通常, 当普通子句集的子句数与变量数的比值较小时, 求解其所不能扩展出的极大项集所得EPCCL理论的规模要远远大于输入子句集, 因此, 直接对普通子句集操作能够加快合并过程.基于此, 我们设计了新的并行EPCCL理论求并算法, 称其为imp-PIAE, 描述如下.

算法3. imp-PIAE.

1.输入:s个EPCCL理论{E1, …, Es}, F1, …, Fs是分别与E1, …, Es所不能扩展出的极大项集等价的普通子句集

2. E=E1, h=2

3. While hs

4.   Divide E to $\{E_{h}^{1},...,E_{h}^{k}\}$

5.   Parallel

6.   Foreach $E_{h}^{k}$ (1≤vk)

7.     d=1

8.     While d≤|$E_{h}^{k}$|

9.       Tv=CIF(Fh, Cd) (Cd$E_{h}^{v}$)

10.       d++

11.   End parallel

12.   E=T1∪…∪Tk

13.   h++

14. Return E

Sub-procedure CIF (CNF F={C1, …, Cn}, clause C)

1.令F1={C}, F2=∅, i=j=k=1

2. While i≤|F|

3.   Si={¬Ci的互补展开} //JM(□)-JM(Ci), 变量集M包含了F中出现的所有变量

4.   While j≤|F1|

5.     If CiCj互补Then skip

6.     Else

7.       While k≤|Ci|

8.       If Si[k]与Cj互补Then skip

9.       Else if Si[kCj Then F2=F2∪{Cj}

10.       Else if Cj‘Si[k] Then F2=F2∪{Si[k]}

11.       Else F2=F2∪{Cj∨(Si[k]-Cj)}

12.       k++

13.     j++

14.     k=1

15.   F1=F2

16.   F2=∅

17.   i++

18.   j=1

19. Return F1

算法3的执行过程与算法2大致相同.不同之处在于:算法3第9行利用了子程序CIF, 而算法2调用了子程序ICE.子程序CIF的功能是计算任意子句与任意子句集所不能扩展出的极大项集的交集, 输出结果为一个EPCCL理论.CIF算法的过程是IKCHER算法的子过程, 其正确性可参照定理5的证明.

4.2 两种并行的IKCHER算法

从IKCHER算法的求解过程中不难看出, 可以对求交知识编译过程进行拆分以实现并行执行.对于输入子句集F={C1, …, Cn}, 有两种并行方式.

1) 利用互补展开求得Fn个子句分别所不能扩展出的极大项集{¬C1}, …, {¬Cn}, 然后利用PIAE并行合并这n个EPCCL理论, 所得结果为F所不能扩展出的极大项集.再次利用上述过程即可求得与F等价的EPCCL理论, 这种方式至少需要n次并行化, 因此, 并行编译过程拆分和合并需要较大开销.

2) 对于任意子句集F={C1, …, Cn}, 将F划分为k个子集F1, …, Fk, 并行求出任意F子集Fi所不能扩展出的极大项集, 所得结果用EPCC理论Ei保存, 然后利用PIAE并行合并F子集对应的k个EPCCL理论.再次利用上述过程即可求得与F等价的EPCCL理论, 这种方式只需要4次并行化, 因此, 本文结合PIAE采用该方式进行IKCHER算法的并行化.

算法4. P-IKCHER.

1.输入:子句集F={C1, …, Cn}

2. t=1

3. Divide F to {F1, …, Fk}

4. Parallel

5. Foreach Fh(1≤hk)

6.   Eh=CKCHER(Fh)

7. End parallel

8. E=PIAE(E1, …, Ek)

9. If t=1 Then

10.   t--

11.   F=E

12.   Goto 3

13. Else return E

Sub-procedure CKCHER (CNF F={C1, …, Cn})

1. h=1

2.初始化:F2={¬C1}, F3=∅, i=2, j=k=1

3. While i≤|F1|

4.   Si={¬Ci的互补展开} //JM(□)-JM(Ci), 变量集M包含了F中出现的所有变量

5.   While j≤|F2|

6.     If CiCj互补Then skip

7.     Else

8.       While k≤|Ci|

9.         If Si[k]与Cj互补Then skip

10.         Else if Si[kCj Then Σ3=Σ3∪{Cj}

11.         Else if Cj‘Si[k] Then Σ3=Σ3∪{Si[k]}

12.         Else Σ3=Σ3∪{Cj∨(Si[k]-Cj)}

13.         k++

14.     j++

15.     k=1

16.   F2=F3

17.   F3=∅

18.   i++

19.   j=1

20. Return F2

算法4采用PIAE策略进行EPCCL理论的并行求交知识编译.该算法中, 第6行的CKCHER子程序用来计算任意子句集所不能扩展出的极大项集, 所得结果为EPCCL理论, 该过程为IKCHER算法的子过程; 第8行的PIAE子程序的具体过程参照第3节中的算法2.P-IKCHER算法采用的策略是:先将输入子句集分割成k个子集, 体现在算法4的第3行; 然后并行求得各个子集所不能扩展出的极大项集, 所得结果为EPCCL理论, 体现在算法4的第4行~第7行; 最后, 利用PIAE算法将所有的EPCCL理论求交, 所得结果就是与输入子句集整体所不能扩展出的极大项集等价的EPCCL理论.另外, 该算法中用t控制求解出与原子句集等价的EPCCL理论.

在利用扩展规则对子句集进行编译的过程中, 子句的长度会随着编译的过程不断增加, 子句的长度增加后, 其所能扩展出的极大项数会减少, 扩展能力会降低.P-IKCHER算法在对输入子句集的子集编译后, 采用PIAE求交策略对子任务所得的EPCCL理论进行合并.求交过程中, 保留了大量子任务输出EPCCL理论中的长子句.这些长子句扩展能力低, 因此会需要更多的长子句来得到与输入子句集等价的EPCCL理论.而且并行算法使用的核数越多, 得到的长子句就越多, 进而编译效果和编译效率会越差.因而可预见的是:利用P-IKCHER算法并行编译所得结果规模会增加, 编译效率相对于串行程序会有所降低.

算法5. impP-IKCHER.

1.输入:子句集F={C1, …, Cn}

2. t=1

3. Divide F to {F1, F2}

4. E=CKCHER(F1)

5. F=imp-PIAE(E, F2)

6. If t=1 Then

7.   t--

8.   F=E

9.   Goto 3

10. Else return F

算法5采用imp-PIAE策略进行EPCCL理论的并行求交知识编译.该算法中, CKCHER子程序与算法4中的CKCHER子程序执行过程相同, 第5行的imp-PIAE子程序的具体过程参照第3节中的算法3.在算法5中, 首先求得输入子句集中部分子句所不能扩展出的极大项集, 并将结果保存为EPCCL理论; 然后对利用imp-PIAE算法对所得到的EPCCL理论和剩余子句集进行并行求交操作, 得到输入子句集所不能扩展出的极大项对应的EPCCL理论; 然后对该EPCCL理论进行相同的操作, 得到与输入子句集等价的EPCCL理论.同样地, 该算法中, 用t控制求解出与原子句集等价的EPCCL理论.

impP-IKCHER算法利用imp-PIAE策略对所得的EPCCL理论进行求交操作, 根据定理6以及IKCHER算法的执行过程不难看出, impP-IKCHER算法是将IKCHER算法中不影响最终结果的可以并行的操作并行化执行.因此可以预见的是, imp-IKCHER算法不会改变IKCHER算法的编译结果的规模, 而且还能提升IKCHER算法的编译效率.

5 IKCHER算法并行效果的测试

UKCHER算法是另一种可并行的知识编译算法, 然而其并行化的工作尚未实现, 并且其编译效率和编译质量远差于IKCHER算法(实验结果见第3节), 因此本文仅对比测试了impP-IKCHER算法、P-IKCHER算法和IKCHER算法的编译效果, 以此验证EPCCL理论并行编译的可行性.本文按照子句数/变量数 4.3的比例生成了若干在相变点附近的3-SAT实例.并行算法用多核算法设计实现, 用k表示任务的划分粒度.

由于P-IKCHER算法是本文设计的一种值得借鉴的有瑕疵的并行算法, 该算法所使用的核数越多, 效果越差, 因此本节对该算法只测试k=2的并行效果.实验结果为50次实验的平均值, 结果见表 7.

Table 7 Experimental results on random 3-SAT instances with n/m≈4.3 表 7 n/m≈4.3的随机3-SAT实例测试

从编译质量来看, 表 7中, 对于所有实例, impP-IKCHER(k=4), impP-IKCHER(k=2) 的编译质量与IKCHER算法均一样; P-IKCHER算法相对于IKCHER算法, 编译质量有所下降.这是由于impP-IKCHER算法先将部分子句集编译为EPCCL理论, 然后在合并过程采用imp-PIAE对已编译的EPCCL理论以及剩余未编译的原始子句集进行并行求交, 这一系列过程与IKCHER算法的执行流程类似, 不同之处在于, impP-IKCHER算法是将IKCHER算法中不影响最终结果的可以并行的操作并行化执行; P-IKCHER算法先将原始子句集分为若干子集, 然后求得这些子集所不能扩展出的EPCCL理论, 再将这些EPCCL理论并行求交, 再求得子集所不能扩展出的极大项后会改变原始子句集的结构, 因此在合并之后很难得到与IKCHER算法相同的结果.而且由于EPCCL理论中子句的长度普遍要长于原始子句集中子句的长度, 因此合并之后, P-IKCHER算法包含了较多的长子句, 这些长子句所能扩展出的极大项集的规模较小, 因此需要更多的长子句来表示原有子句集, 从而P-IKCHER算法的编译规模会大于impP-IKCHER算法和IKCHER算法的编译规模.

从编译效率上看, 表 7中, impP-IKCHER(k=4) 和impP-IKCHER(k=2) 均起到了一定的加速效果, 然而加速效果并不明显, 当k=4时, 最大加速比仅为2倍(如表 1中, 〈27, 116〉, 〈30, 128〉, 〈34, 146〉和blockworld-anomaly等实例), 这是由于本文分配任务的策略采用的是按子句数划分, 这种划分策略并未考虑到子句集本身的内在结构, 因此负载均衡较差; P-IKCHER(k=2) 未起到加速效果, 反而降低了编译效率, 其原因正在于它采用PIAE算法直接合并多个EPCCL理论, 极大地增加了编译过程所需时间开销.

整体来看, impP-IKCHER能够提高P-IKCHER算法的编译效率.原始IKCHER算法的编译效率稍弱于DKCHER算法的编译效率, 但由于impP-IKCHER算法采用了合适的并行合并策略, 使求交知识编译方法的编译效率得到了提高(当k=2时, impP-IKCHER算法的编译效率已经明显高于DKCHER算法的编译效率).因此, 采用合适的并行合并策略之后, IKCHER算法的并行化是可行的, 这一点能够为其他目标编译语言的并行编译提供借鉴.

6 结论与展望

本文提出了一种新的EPCCL理论编译算法——求交知识编译算法IKCHER, 并设计了两种EPCCL理论的并行求交算法PIAE和imp-PIAE, 其中, imp-PIAE利用了输入EPCCL理论对于所不能扩展出极大项集的原始子句集.基于PIAE算法和imp-PIAE算法, 提出了两种并行求交知识编译算法P-IKCHER和impP-IKCHER.实验结果表明, IKCHER算法有最优的编译质量以及接近最优的编译效率, 而impP-IKCHER能够提高IKCHER算法的编译效率, P-IKCHER算法的编译效率相对于IKCHER算法反而有所降低, 说明了合适的合并策略对于知识编译算法的并行化至关重要.本文的研究成果验证了并行知识编译是可行的, 该成果同时能够为其他目标语言编译算法的并行化提供借鉴.

未来, 我们将研究如何进一步提高EPCCL理论合并算法的效率, 并使impP-IKCHER算法有更广的应用范围.本文中, 对输入子句集的分割采用了等子句数分割, 而分割结果会影响负载均衡及并行算法的整体执行效率, 因此, 任务分割的启发式选择也将是下一步的研究重点.

参考文献
[1] Cook SA. The complexity of theorem-proving procedures. In:Harrison MA, Banerji RB, Ullman JD, eds. Proc. of the 3rd Annual ACM Symp. on the Theory of Computing (STOC'71). Shaker Heights:ACM Press, 1971. 151-158.[doi:10.1145/800157.805047]
[2] Mitchell DG, Selman B, Levesque HJ. Hard and easy distributions of SAT problems. In:Swartout WR, ed. Proc. of the 10th National Conf. on Artificial Intelligence (AAAI'92). San Jose:AAAI Press, The MIT Press, 1992. 459-465.
[3] Bai S, Bu DB. Analysis for phase transition of the 2-3-SAT problem. Ruan Jian Xue Bao/Journal of Software, 1998, 9(11): 828–832 (in Chinese with English abstract). http://www.jos.org.cn/ch/reader/view_abstract.aspx?flag=1&file_no=19981106&journal_id=jos [doi:10.13328/j.cnki.jos.1998.11.006]
[4] Cai SW, Su KL. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013, 204: 75–98 . [doi:10.1016/j.artint.2013.09.001]
[5] Luo C, Su KL, Cai SW. More efficient two-mode stochastic local search for random 3-satisfiability. Applied Intelligence, 2014, 41(3): 665–680 . [doi:10.1007/s10489-014-0556-7]
[6] Luo C, Cai SW, Wu W, Su KL. Double configuration checking in stochastic local search for satisfiability. In:Brodley CE, Stone P, eds. Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI 2014). Québec:AAAI Press, 2014. 2703-2709.
[7] Cai SW, Su KL. Comprehensive score:Towards efficient local search for SAT with long clauses. In:Rossi F, ed. Proc. of the 23rd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI Press, 2013. 489-495.
[8] Jeavons P, Petke J. Local consistency and SAT-solvers. Journal of Artificial Intelligence Research, 2012, 43: 329–351 . [doi:10.1613/jair.3531]
[9] Katsirelos G, Sabharwal A, Samulowitz H, Simon L. Resolution and parallelizability:Barriers to the efficient parallelization of SAT solvers. In:desJardins M, Littman ML, eds. Proc. of the 27th AAAI Conf. on Artificial Intelligence (AAAI 2013). Washington:AAAI Press, 2013.
[10] Audemard G, Simon L. Lazy clause exchange policy for parallel SAT solvers. In Sinz C, Egly U, eds. Proc. of the 17th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2014). LNCS 8561, Vienna:Springer-Verlag, 2014. 197-205.[doi:10.1007/978-3-319-09284-3_15]
[11] Sonobe T, Kondoh S, Inaba M. Community branching for parallel portfolio SAT solvers. In Sinz C, Egly U, eds. Proc. of the 17th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2014). LNCS 8561, Vienna:Springer-Verlag, 2014. 188-196.[doi:10.1007/978-3-319-09284-3_14]
[12] Val DA. On some tractable classes in deduction and abduction. Artificial Intelligence, 2000, 116(1-2): 297–313 . [doi:10.1016/S0004-3702(99)00088-0]
[13] Broeck GV, Darwiche A. On the role of canonicity in knowledge compilation. In:Bonet B, Koenig S, eds. Proc. of the 29th AAAI Conf. on Artificial Intelligence (AAAI 2015). Austin:AAAI Press, 2015. 1641-1648.
[14] Marquis P. Existential closures for knowledge compilation. In:Walsh T, ed. Proc. of the 22nd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2011). Barcelona:IJCAI/AAAI Press, 2011. 996-1001.[doi:10.5591/978-1-57735-516-8/IJCAI11-171]
[15] Fargier H, Marquis P. Disjunctive closures for knowledge compilation. Artificial Intelligence, 2014, 216: 129–162 . [doi:10.1016/j.artint.2014.07.004]
[16] Darwiche A. Compiling knowledge into decomposable negation normal form. In:Dean T, ed. Proc. of the 16th Int'l Joint Conf. on Artificial Intelligence (IJCAI'99). Stockholm:Morgan Kaufmann Publishers, 1999. 284-289.
[17] Darwiche A. Decomposable negation normal form. Journal of the ACM, 2001, 48(4): 608–647 . [doi:10.1145/502090.502091]
[18] Darwiche A, Marquis P. A knowledge compilation map. Journal of Artificial Intelligence Research, 2002, 17: 229–264 . [doi:10.1613/jair.989]
[19] Fargier H, Marquis P. Extending the knowledge compilation map:Krom, Horn, Affine and beyond. In:Fox D, Gomes CP, eds. Proc. of the 23rd AAAI Conf. on Artificial Intelligence (AAAI 2008). Chicago:AAAI Press, 2008. 442-447.
[20] Fargier H, Marquis P, Niveau A. Towards a knowledge compilation map for heterogeneous representation languages. In:Rossi F, ed. Proc. of the 23rd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI Press, 2013. 877-883.
[21] Fargier H, Marquis P, Niveau A, Schmidt N. A knowledge compilation map for ordered real-valued decision diagrams. In:Brodley CE, Stone P, eds. Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI 2014). Québec:AAAI Press, 2014. 1049-1055.
[22] Koriche F, Lagniez JM, Marquis P, Thomas S. Knowledge compilation for model counting:Affine decision trees. In:Rossi F, ed. Proc. of the 23rd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI Press, 2013. 947-953.
[23] Lai Y, Liu DY, Wang SS. Reduced ordered binary decision diagram with implied literals:A new knowledge compilation approach. Knowledge and Information Systems, 2013, 35(3): 665–712 . [doi:10.1007/s10115-012-0525-6]
[24] Huang JB, Darwiche A. The language of search. Journal of Artificial Intelligence Research, 2007, 29: 191–219 . [doi:10.1613/jair.2097]
[25] Lin H, Sun JG, Zhang YM. Theorem proving based on the extension rule. Journal of Automated Reasoning, 2003, 31(1): 11–21 . [doi:10.1023/A:1027339205632]
[26] Yin MH, Lin H, Sun JG. Solving #SAT using extension rules. Ruan Jian Xue Bao/Journal of Software, 2009, 20(7): 1714–1725 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3320.htm [doi:10.3724/SP.J.1001.2009.03320]
[27] Lai Y, Ouyang DT, Cai DB, Lü S. Model counting and planning using extension rule. Journal of Computer Research and Development, 2009, 46(3): 459–469 (in Chinese with English abstract). http://www.cnki.com.cn/Article/CJFDTOTAL-JFYZ200903016.htm
[28] Li Y, Sun JG, Wu X, Zhu XJ. Extension rule algorithms based on IMOM and IBOHM heuristics strategies. Ruan Jian Xue Bao/Journal of Software, 2009, 20(6): 1521–1527 (in Chinese with English abstract). [doi:10.3724/SP.J.1001.2009.03420]
[29] Sun JG, Li Y, Zhu XJ, Lü S. A novel theorem proving algorithm based on extension rule. Journal of Computer Research and Development, 2009, 46(1): 9–14 (in Chinese with English abstract). http://www.cnki.com.cn/Article/CJFDTOTAL-JFYZ200901003.htm
[30] Lin H, Sun JG. Knowledge compilation using the extension rule. Journal of Automated Reasoning, 2004, 32(2): 93–102 . [doi:10.1023/B:JARS.0000029959.45572.44]
[31] Yin MH, Lin H, Sun JG. Counting models using extension rules. In:Proc. of the 22nd AAAI Conf. on Artificial Intelligence (AAAI 2007). Vancouver:AAAI Press, 2007. 1916-1917.
[32] Gu WX, Wang JY, Yin MH. Knowledge compilation using extension rule based on MCN and MO heuristic strategies. Journal of Computer Research and Development, 2011, 48(11): 2064–2073 (in Chinese with English abstract). http://www.cnki.com.cn/Article/CJFDTOTAL-JFYZ201111018.htm
[33] Liu DY, Lai Y, Lin H. C2E:An EPCCL compiler with good performance. Chinese Journal of Computers, 2013, 36(6): 1254–1260 (in Chinese with English abstract). [doi:10.3724/SP.J.1016.2013.01254]
[34] Liu L, Niu DD, Li Z, Lü S. Dynamic online reasoning algorithm based on the hyper extension rule. Journal of Harbin Engineering University, 2015, 36(12): 1614–1619 (in Chinese with English abstract). [doi:10.11990/jheu.201404055]
[35] Liu L, Niu DD, Lü S. Knowledge compilation methods based on the hyper extension rule. Chinese Journal of Computers, 2016, 39(8): 1681–1696 (in Chinese with English abstract). [doi:10.11897/SP.J.1016.2016.01681]
[3] 白硕, 卜东波. 2-3-SAT问题相变现象剖析及其应用. 软件学报, 1998, 9(11): 828–832. http://www.jos.org.cn/ch/reader/view_abstract.aspx?flag=1&file_no=19981106&journal_id=jos [doi:10.13328/j.cnki.jos.1998.11.006]
[26] 殷明浩, 林海, 孙吉贵. 一种基于扩展规则的#SAT求解系统. 软件学报, 2009, 20(7): 1714–1725. http://www.jos.org.cn/1000-9825/3320.htm [doi:10.3724/SP.J.1001.2009.03320]
[27] 赖永, 欧阳丹彤, 蔡敦波, 吕帅. 基于扩展规则的模型计数与智能规划方法. 计算机研究与发展, 2009, 46(3): 459–469. http://www.cnki.com.cn/Article/CJFDTOTAL-JFYZ200903016.htm
[28] 李莹, 孙吉贵, 吴瑕, 朱兴军. 基于IMOM和IBOHM启发式策略的扩展规则算法. 软件学报, 2009, 20(6): 1521–1527. [doi:10.3724/SP.J.1001.2009.03420]
[29] 孙吉贵, 李莹, 朱兴军, 吕帅. 一种新的基于扩展规则的定理证明方法. 计算机研究与发展, 2009, 46(1): 9–14. http://www.cnki.com.cn/Article/CJFDTOTAL-JFYZ200901003.htm
[32] 谷文祥, 王金艳, 殷明浩. 基于MCN和MO启发式策略的扩展规则知识编译方法. 计算机研究与发展, 2011, 48(11): 2064–2073. http://www.cnki.com.cn/Article/CJFDTOTAL-JFYZ201111018.htm
[33] 刘大有, 赖永, 林海. C2E:一个高性能的EPCCL理论编译器. 计算机学报, 2013, 36(6): 1254–1260. [doi:10.3724/SP.J.1016.2013.01254]
[34] 刘磊, 牛当当, 李壮, 吕帅. 基于超扩展规则的动态在线推理算法. 哈尔滨工程大学学报, 2015, 36(12): 1614–1619. [doi:10.11990/jheu.201404055]
[35] 刘磊, 牛当当, 吕帅. 基于超扩展规则的知识编译方法. 计算机学报, 2016, 39(8): 1681–1696. [doi:10.11897/SP.J.1016.2016.01681]