• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Conference on Tools with Artificial Intelligence >From Set Constraint Models to SAT Instances
【24h】

From Set Constraint Models to SAT Instances

机译：从集合约束模型到SAT实例

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

On the one hand, Constraint Satisfaction Problems (CSP) are a declarative and expressive approach for modeling problems. On the other hand, propositional satisfiability problem (SAT) solvers can handle huge SAT instances up to millions of variables and clauses. In this article, we present an approach for taking advantage of both CSP modeling and SAT solving. Our technique consists in expressively modeling set constraint problems as CSPs that are automatically treated by some reduction rules to remove values that do not participate in any solution. These reduced CSPs are then encoded into ”good” SAT instances that can be solved by standard SAT solvers. We illustrate our technique on the Sports Tournament Scheduling problem, and we show that we obtain competitive results compared to an adhoc solver. Our technique is simpler, more expressive, and less error-prone than direct SAT modeling. The SAT instances that we automatically generate are rather small and can efficiently be solved up to huge instances. Moreover, the reduction phase enables to push back the limits and treat even larger problems.
机译：一方面，约束满足问题（CSP）是一种用于建模问题的声明性和表达性方法。另一方面，命题可满足性问题（SAT）求解器可以处理多达数百万个变量和子句的巨大SAT实例。在本文中，我们提出了一种利用CSP建模和SAT求解的方法。我们的技术包括将集约束问题作为CSP进行表达建模，并通过一些归约规则自动处理以消除不参与任何解决方案的值。然后将这些缩减的CSP编码为“好” SAT实例，可以通过标准SAT解算器进行求解。我们举例说明了有关运动锦标赛调度问题的技术，并表明与自组织求解器相比，我们获得了竞争性结果。与直接SAT建模相比，我们的技术更简单，更具表现力且更不易出错。我们自动生成的SAT实例很小，可以有效地解决大型实例。此外，减少阶段可以减少限制并处理更大的问题。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号