首页> 外文期刊>Journal of multiple-valued logic and soft computing >Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions
【24h】

Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions

机译:计算最小不满意的子公式:最新技术和未来方向

获取原文
获取原文并翻译 | 示例
           

摘要

The task of modeling and reasoning about real-world problems often involves analyzing over-constrained representations, where not all constraints of a problem can be simultaneously satisfied. The need to analyze over-constrained (or unsatisliable) problems occurs in many settings, including data and knowledge bases, artilicial intelligence, applied formal methods, operations research and description logics. In most cases, the problem to solve is related with some form of minimal unsatisfiability, i.e. an irreducible set of constraints that explains unsatisliability. This paper provides an overview of algorithms for computing minimally unsatisliable subformulas, and conducts an experimental evaluation of these algorithms. In addition, the paper briefly overviews computational problems related with minimal unsatisfiability in Boolean logic, practical applications of minimal unsatisfiability, and extensions of minimal unsatisfiability to other domains.
机译:对现实问题进行建模和推理的任务通常涉及分析过度约束的表示,在这种情况下,问题的所有约束不能同时得到满足。在许多情况下都需要分析过度约束(或无法满足)的问题,包括数据和知识库,人工智能,应用的形式方法,运筹学和描述逻辑。在大多数情况下,要解决的问题与某种形式的最小不满足性有关,即,一组不可约的约束说明了不满足性。本文概述了用于计算最小不满足子公式的算法,并对这些算法进行了实验评估。另外,本文简要概述了与布尔逻辑中的最小不满足性,最小不满足性的实际应用以及最小不满足性向其他域的扩展有关的计算问题。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号