一种EPCCL理论编译算法

　　超扩展规则是对扩展规则的扩充，基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集，并将所得结果以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倍．