• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Expert systems with applications >Solving complex problems using model transformations: from set constraint modeling to SAT instance solving
【24h】

Solving complex problems using model transformations: from set constraint modeling to SAT instance solving

机译：使用模型转换解决复杂问题：从集合建模到SAT实例求解

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

摘要

On the one hand, solvers for the propositional satisfiability problem (SAT) can deal with huge instances composed of millions of variables and clauses. On the other hand, Constraint Satisfaction Problems (CSP) can model problems as constraints over a set of variables with non-empty domains. They require combinatorial search methods as well as heuristics to be solved in a reasonable time.In this article, we present a technique that benefits from both expressive CSP modeling and efficient SAT solving. We model problems as CSP set constraints. Then, a propagation algorithm reduces the domains of variables by removing values that cannot participate in any valid assignment. The reduced CSP set constraints are transformed into a set of suitable SAT instances. They may be simplified by a preprocessing method before applying a standard SAT solver for computing their solutions.The practical usefulness of this technique is illustrated with two well-known problems: a) the Social Golfer, and b) the Sports Tournament Scheduling. We obtained competitive results either compared with ad hoc solvers or with hand-written SAT instances. Compared with direct SAT modeling, the proposed technique offers higher expressiveness, is less error-prone, and is relatively simpler to apply. The automatically generated propositional satisfiability instances are rather small in terms of clauses and variables. Hence, applying the constraint propagation phase, even huge instances of our problems can be tackled and efficiently solved. (C) 2020 Elsevier Ltd. All rights reserved.
机译：一方面，主命出可满足性问题（SAT）的求解器可以处理由数百万变量和条款组成的巨大实例。另一方面，约束满足问题（CSP）可以将问题模拟为具有非空域的一组变量的限制。它们需要组合搜索方法以及在合理的时间内解决的启发式。在本文中，我们提出了一种从富有表现力的CSP建模和高效饱和的技术中受益的技术。我们模拟了CSP集约束的问题。然后，传播算法通过删除无法参与任何有效分配的值来减少变量的域。减少的CSP集约束被转换为一组合适的SAT实例。在应用标准SAT求解器之前，可以通过预处理方法简化它们，以计算它们的解决方案。这种技术的实际有用性用两个众所周知的问题说明：a）社会高尔夫球手和b）体育比赛调度。我们与Ad Hoc求解器或手写的SAT实例相比，我们获得了竞争力。与直接饱和建模相比，所提出的技术具有更高的效果，易于出错，并且应用相对更简单。在条款和变量方面，自动生成的命题可满足性实例相当小。因此，应用约束传播阶段，即使是我们问题的巨大实例也可以解决和有效地解决。 （c）2020 elestvier有限公司保留所有权利。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号