C2E:一个高性能的EPCCL编译器

摘要

The EPCCL theory is a new kind of target language for knowledge compilation.In this paper,we propose a new knowledge compilation algorithm KCDP that compiles a CNF formula into an EPCCL theory.KCDP is based on the DPLL procedure,which is the basis of most complete SAT solvers.KCDP provides a bridge between EPCCL theory and SAT so that most of the available techniques about the DPLL procedure can be easily introduced into the compilation of EPCCL theory.Furthermore,we propose an algorithm called REDUCE to simplify an EPCCL theory.The REDUCE is based on the reduction rule,which can be seen as a special kind of resolution.Finally,we devise an EPCCL compiler C2E to combine the strength of KCDP and REDUCE,and we test its performances on random instances and benchmarks.The experimental results show that C2E is an EPCCL compiler with good performance.%提出一个新的基于DPLL的编译算法KCDP,从而成功地将EPCCL理论和SAT求解联系起来,使得目前很多应用在基于DPLL的SAT求解器中先进的技术都能被引入到EPCCL理论的编译中以提高编译效率;提出规约规则,并基于该规则,提出能在多项式时间内终止的REDUCE算法对EPCCL理论进行规约;结合KCDP和REDUCE算法,实现了编译器C2E,并在随机问题和国际通用的测试用例上测试了C2E的编译效率和编译质量,实验结果表明,无论从编译效率还是编译质量来说,C2E都是一个高性能的EPCCL编译器.