• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >Improving IntSat by expressing disjunctions of bounds as linear constraints
【24h】

Improving IntSat by expressing disjunctions of bounds as linear constraints

机译：通过将边界的分离表示为线性约束来改善IntSat

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

摘要

Conflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates no strong enough ILP constraint, and the backjump has to be done based on the conflicting set of bounds. The techniques given in this article precisely analyze how and when that set can be translated into the required new ILP constraint. Moreover, this can be done efficiently. This obviously strengthens learning and significantly improves the performance of IntSat (as confirmed by our experiments). We also briefly discuss extensions and other applications.
机译：冲突驱动子句学习（CDCL）SAT解算器可以自动解决非常大的现实问题。 IntSat是一项将CDCL扩展到整数线性编程（ILP）的新技术。对于某些冲突，IntSat不会生成足够强的ILP约束，因此必须基于冲突的边界集进行回跳。本文中给出的技术可以精确地分析如何以及何时将该集合转换为所需的新ILP约束。而且，这可以有效地完成。这显然加强了学习并显着提高了IntSat的性能（我们的实验已证实）。我们还将简要讨论扩展和其他应用程序。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号