aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming

Encoding finite linear CSPs as Boolean formulas and solving them by using modern SAT solvers has proven to be highly effective by the award-winning sugar system. We here develop an alternative approach based on ASP that serves two purposes. First, it provides a library for solving CSPs as part of an encompassing logic program. Second, it furnishes an ASP-based CP solver similar to sugar. Both tasks are addressed by using first-order ASP encodings that provide us with a high degree of flexibility, either for integration within ASP or for easy experimentation with different implementations. When used as a CP solver, the resulting system aspartame re-uses parts of sugar for parsing and normalizing CSPs. The obtained set of facts is then combined with an ASP encoding that can be grounded and solved by off-the-shelf ASP systems. We establish the competitiveness of our approach by empirically contrasting aspartame and sugar.