• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >Algorithms for computing backbones of propositional formulae
【24h】

Algorithms for computing backbones of propositional formulae

机译：计算命题公式主干的算法

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

摘要

The problem of propositional satisfiability (SAT) has found a number of applications in both theoretical and practical computer science. In many applications, however, knowing a formula's satisfiability alone is insufficient. Often, some other properties of the formula need to be computed. This article focuses on one such property: the backbone of a formula, which is the set of literals that are true in all the formula's models. Backbones find theoretical applications in characterization of SAT problems and they also find practical applications in product configuration or fault localization. This article overviews existing algorithms for backbone computation and introduces two novel ones. Further, an extensive evaluation of the algorithms is presented. This evaluation demonstrates that one of the novel algorithms significantly outperforms the existing ones.
机译：命题可满足性（SAT）问题已在理论和实践计算机科学中找到了许多应用。但是，在许多应用程序中，仅了解公式的可满足性是不够的。通常，需要计算公式的其他一些属性。本文着重介绍这样一个属性：公式的主干，即在所有公式模型中都适用的一组文字。骨干在表征SAT问题中找到了理论应用，并且在产品配置或故障定位中也找到了实际应用。本文概述了现有的骨干计算算法，并介绍了两种新颖的算法。此外，提出了对该算法的广泛评估。该评估表明，一种新颖的算法明显优于现有算法。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号