关于某些 CNF 理论最小模型计算的可处理性
人工智能
2013-10-31 v1 计算机科学中的逻辑
摘要
设计能够高效构建 CNF 最小模型的算法是人工智能中的一项重要任务。本文沿此研究路线提供了新结果，并提出了用于在正命题 CNF 上执行最小模型查找与检查以及在命题 CNF 上进行模型最小化的新算法。我们提出了一种称为广义消除算法 (GEA) 的算法模式，用于计算任意正 CNF 的最小模型。该模式推广了消除算法 (EA) [BP97]，后者计算正头循环自由 (HCF) CNF 理论的最小模型。虽然 EA 在输入 HCF CNF 的规模上始终以多项式时间运行，但 GEA 的复杂度取决于其中调用的特定消除算子的复杂度，这在一般情况下可能是指数的。因此，我们定义了一个特定的消除算子，使得 GEA 能在多项式时间内为一类 CNF 计算最小模型，该类 CNF 严格包含头基本集自由 (HEF) CNF 理论 [GLL06]，而后者本身又是 HCF 理论的严格超集。此外，为了应对识别 HEF 理论相关的高复杂度问题，我们提出了 GEA 的一种“不完全”变体（称为 IGEA）：所得模式一旦实例化为适当的消除算子，总能构建输入 CNF 的一个模型，且若输入理论为 HEF，则保证该模型是最小的。鉴于上述结果，本文的主要贡献是扩大了最小模型查找与检查以及模型最小化问题的可处理性边界。
引用
@article{arxiv.1310.8120,
title = {On the Tractability of Minimal Model Computation for Some CNF Theories},
author = {Fabrizio Angiulli and Rachel Ben-Eliyahu-Zohary and Fabio Fassetti and Luigi Palopoli},
journal= {arXiv preprint arXiv:1310.8120},
year = {2013}
}