A system for CSP solving through satisfiability Modulo theories
Miquel Bofill, Miquel Palahí, Mateu Villaret · 2009
In this paper we discuss work in progress on the design and implementation of Simply, a system for modeling and solving Constraint Satisfaction Problems (CSP). During the last years, there has been a dramatic improvement on performance of SAT solvers, and solving CSPs by translation into propositional formulas has become a real choice in many cases. The advances in SAT technology have been adapted for more expressive (yet decidable) logics, e.g., in the framework of SAT Modulo Theories (SMT). Simply is intended to be a declarative programming system for easy CSP modeling which generates SMT formulas for solving these CSP. The utility and interest of Simply is twofold: on the one hand, it serves as a benchmark generator for CSP solving with different state-of-the-art SMT solvers and, on the other hand, the system aims at taking advantage of the highly increasing performance of these solvers.