Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems

Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems
复制标题

Scarab：基于 SAT 的约束编程系统的快速原型设计工具

DOI：
10.1007/978-3-642-39071-5_34
复制
发表时间：
2013
期刊：
Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013)
影响因子：
--
通讯作者：
and Mutsunori Banbara
and Mutsunori Banbara
中科院分区：
--
文献类型：
--
作者：
Takehide Soh;Naoyuki Tamura;and Mutsunori Banbara

文献摘要

相似文献

在本文中，我们提出了圣甲虫系统，这是一个原型工具，用于开发基于SAT的系统。它在Scala上提供了丰富的约束建模语言，使程序员能够快速指定问题并尝试不同的建模。Scarab还提供了一种简单的方法来实现增量求解，解决方案枚举，以及动态添加和/或删除约束。在Scarab中，我们可以使用整数变量和算术约束，并且所有这些都被编码到SAT中，而不需要开发专用的编码器。SAT解算器用于寻找解决方案。
In this paper, we present the Scarab system which is a prototyping tool for developing SAT-based systems. It provides a rich constraint modeling language on Scala and enables a programmer to rapidly specify problems and to experiment with different modelings. Scarab also provides a simple way to realize incremental solving, solution enumeration, and dynamic addition and/or removal of constraints. In Scarab, we can use integer variables and arithmetic constraints, and all of them are encoded into SAT without the need of developing dedicated encoder. SAT solvers are then used for finding solutions.