CoAPI：一种基于核心引导过近似覆盖的非子句公式素编译高效两阶段算法
人工智能
2019-06-10 v1 计算机科学中的逻辑
摘要
素编译，即生成公式的所有素蕴涵项或素隐含项（简称素），是人工智能中一个突出的基础问题。近年来，非子句公式的素编译受到了极大关注。现有最优方法利用双轨编码由素蕴涵项构造素覆盖并生成所有素。然而，双轨编码可能扩展搜索空间。此外，构造其方法所必需的素覆盖十分耗时。为解决这些问题，我们提出一种新颖的两阶段方法——CoAPI。这两个阶段是无需使用双轨编码构造覆盖的关键。具体而言，给定非子句公式，我们在第一阶段提出一种核心引导方法，将非子句公式重写为由过近似蕴涵项构造的覆盖；随后在第二阶段基于该覆盖生成所有素。为减小覆盖规模，我们提供了一种基于多序的压缩方法，在小规模与效率之间取得良好权衡，显著压缩覆盖规模。实验结果表明，CoAPI 优于现有最优方法。特别地，在生成所有素蕴涵项方面，CoAPI 耗时约少一个数量级。
引用
@article{arxiv.1906.03085,
title = {CoAPI: An Efficient Two-Phase Algorithm Using Core-Guided Over-Approximate Cover for Prime Compilation of Non-Clausal Formulae},
author = {Weilin Luo and Hai Wan and Hongzhen Zhong and Ou Wei},
journal= {arXiv preprint arXiv:1906.03085},
year = {2019}
}