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

摘要

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.