• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Constraints >Propagation via lazy clause generation
【24h】

Propagation via lazy clause generation

机译：通过延迟子句生成进行传播

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

摘要

Finite domain propagation solvers effectively represent the possible values of variables by a set of choices which can be naturally modelled as Boolean variables. In this paper we describe how to mimic a finite domain propagation engine, by mapping propagators into clauses in a SAT solver. This immediately results in strong nogoods for finite domain propagation. But a naive static translation is impractical except in limited cases. We show how to convert propagators to lazy clause generators for a SAT solver. The resulting system introduces flexibility in modelling since variables are modelled dually in the propagation engine and the SAT solver, and we explore various approaches to the dual modelling. We show that the resulting system solves many finite domain problems significantly faster than other techniques.
机译：有限域传播求解器通过一组选择可以有效地表示变量的可能值，这些选择可以自然地建模为布尔变量。在本文中，我们描述了如何通过将传播子映射到SAT解算器中的子句中来模拟有限域传播引擎。这立即导致有限域传播的强烈干扰。但是，除少数情况外，单纯的静态翻译是不切实际的。我们展示了如何将传播器转换为SAT求解器的惰性子句生成器。由于变量是在传播引擎和SAT解算器中双重建模的，因此所得的系统在建模方面引入了灵活性，并且我们探索了多种双重建模方法。我们证明，与其他技术相比，所得系统可以更快地解决许多有限域问题。

著录项

  • 来源
    《Constraints》 |2009年第3期|357-391|共35页
  • 作者

    Olga Ohrimenko; Peter J. Stuckey; Michael Codish;

  • 作者单位

    NICTA Victoria Research Lab, Department of Comp. Sci. and Soft. Eng., University of Melbourne, Melbourne, Australia;

    NICTA Victoria Research Lab, Department of Comp. Sci. and Soft. Eng., University of Melbourne, Melbourne, Australia;

    Department of Computer Science, Ben-Gurion University, Beersheba, Israel;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

    finite domain propagation; boolean variables; SAT solver;

    机译：有限域传播;布尔变量;SAT求解器;

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号