• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >Towards backbone computing: A Greedy-Whitening based approach
【24h】

Towards backbone computing: A Greedy-Whitening based approach

机译：迈向骨干计算：基于贪婪美白的方法

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

摘要

Backbone is the set of literals that are true in all formula's models. Computing a part of backbone efficiently could guide the following searching in SAT solving and accelerate the process, which is widely used in fault localization, product configuration, and formula simplification. Specifically, iterative SAT testings among literals are the most time consumer in backbone computing. We propose a Greedy-Whitening based algorithm in order to accelerate backbone computing. On the one hand, we try to reduce the number of SAT testings as many as possible. On the other hand, we make every inventible SAT testing more efficient. The proposed approach consists of three steps. The first step is a Greedy-based algorithm which computes an under-approximation of non-backbone (BL) over bar(Phi). Backbone computing is accelerated since SAT testings of literals in (BL) over bar(Phi) are saved. The second step is a Whitening-based algorithm with two heuristic strategies which computes an approximation set of backbone (BL) over cap(Phi). Backbone computing is accelerated since more backbone are found at an early stage of the computing by testing the literals in (BL) over cap(Phi) first, which makes every individual SAT testing more efficient. The exact backbone is computed in the third step which applies iterative backbone testing on the approximations. We implemented our approach in a tool BONE and conducted experiments on instances from Industrial tracks of SAT Competitions between 2002 and 2016. Empirical results show that BONE is more efficient in industrial and crafted formulas.
机译：骨干是在所有公式模型中均正确的一组文字。有效地计算骨干的一部分可指导SAT解决中的以下搜索并加速该过程，该过程广泛用于故障定位，产品配置和公式简化。具体来说，文字之间的迭代SAT测试是骨干计算中最消耗时间的。我们提出一种基于Greedy-Whitening的算法，以加速骨干计算。一方面，我们尝试减少SAT测试的次数。另一方面，我们使每项发明的SAT测试都更加高效。提议的方法包括三个步骤。第一步是基于贪婪的算法，该算法计算bar（Phi）上非骨干（BL）的欠逼近度。由于节省了bar（Phi）上（BL）中文字的SAT测试，因此可以加快骨干计算的速度。第二步是具有两种启发式策略的基于Whitening的算法，该算法计算cap（Phi）上的主干（BL）近似集。由于在计算的早期阶段通过首先在（BL）over cap（Phi）中测试文字来发现更多的主干，因此加快了骨干计算的速度，这使每个SAT测试效率更高。在第三步中计算出精确的主干，该主干将迭代主干测试应用于近似值。我们在工具BONE中实施了我们的方法，并在2002年至2016年间对SAT竞赛的工业跟踪实例进行了实验。经验结果表明，BONE在工业和人工配方中效率更高。

著录项

  • 来源
    《AI communications》 |2018年第3期|267-280|共14页
  • 作者

    Zhang Yueling; Zhang Min; Pu Geguang; Song Fu; Li Jianwen;

  • 作者单位

    East China Normal Univ, Natl Res Ctr Trustworthy Embedded Software, Shanghai, Peoples R China;

    East China Normal Univ, Natl Res Ctr Trustworthy Embedded Software, Shanghai, Peoples R China;

    East China Normal Univ, Natl Res Ctr Trustworthy Embedded Software, Shanghai, Peoples R China;

    ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai, Peoples R China;

    East China Normal Univ, Natl Res Ctr Trustworthy Embedded Software, Shanghai, Peoples R China;

  • 收录信息 美国《科学引文索引》(SCI);美国《工程索引》(EI);
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

    Backbone; satisfiability; approximation; greedy; whitening;

    机译：骨干;满意度;近似;贪婪;美白;

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号