论文部分内容阅读
提出一个新的基于DPLL的编译算法KCDP，从而成功地将EPCCL理论和SAT求解联系起来，使得目前很多应用在基于DPLL的SAT求解器中先进的技术都能被引入到EPCCL理论的编译中以提高编译效率；提出规约规则，并基于该规则，提出能在多项式时间内终止的REDUCE算法对EPCCL理论进行规约；结合KCDP和REDUCE算法，实现了编译器C2E，并在随机问题和国际通用的测试用例上测试了C2E的编译效率和编译质量，实验结果表明，无论从编译效率还是编译质量来说，C2E都是一个高性能的EPCCL编译器．