• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Artificial intelligence >Enhancing disjunctive logic programming systems by SAT checkers
【24h】

Enhancing disjunctive logic programming systems by SAT checkers

机译：通过SAT检查器增强逻辑逻辑编程系统

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Disjunctive logic programming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. Reasoning with DLP is harder than with normal (v-free) logic programs, because stable model checking - deciding whether a given model is a stable model of a propositional DLP program - is co-NP-complete, while it is polynomial for normal logic programs. This paper proposes a new transformation Γ_M(P), which reduces stable model checking to UNSAT - i.e., to deciding whether a given CNF formula is unsatisfiable. The stability of a model M of a program P thus can be verified by calling a Satisfiability Checker on the CNF formula Γ_(M)(P). The transformation is parsimonious (i.e., no new symbol is added), and efficiently computable, as it runs in logarithmic space (and therefore in polynomial time). Moreover, the size of the generated CNF formula never exceeds the size of the input (and is usually much smaller). We complement this transformation with modular evaluation results, which allow for efficient handling of large real-world reasoning problems. The proposed approach to stable model checking has been implemented in DLV - a state-of-the-art implementation of DLP. A number of experiments and benchmarks have been runusing SATZ as Satisfiability checker. The results of the experiments are very positive and confirm the usefulness of our techniques.
机译：具有稳定模型语义的析取逻辑编程（DLP）是用于知识表示和推理的强大的非单调形式主义。使用DLP进行推理比使用普通（无v型）逻辑程序困难，因为稳定的模型检查（确定给定模型是否是命题DLP程序的稳定模型）是co-NP-完全的，而对于正常逻辑来说是多项式程式。本文提出了一种新的变换Γ_M（P），该变换将稳定的模型检查减少到UNSAT，即确定给定的CNF公式是否不令人满意。因此，可以通过在CNF公式Γ_（M）（P）上调用满意度检查器来验证程序P的模型M的稳定性。变换是对等的（即，未添加新符号），并且可以在对数空间（因此在多项式时间内）运行时有效地进行计算。此外，生成的CNF公式的大小永远不会超过输入的大小（通常小得多）。我们通过模块化评估结果来补充这种转换，从而可以有效处理大型现实推理问题。提出的稳定模型检查方法已经在DLV中实现-DLP的最新实现。使用SATZ作为满意度检查器进行了许多实验和基准测试。实验结果非常积极，证实了我们技术的实用性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号