aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming

Abstract : 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.
Complete list of metadatas

https://hal.inria.fr/hal-01186996
Contributor : René Quiniou <>
Submitted on : Tuesday, August 25, 2015 - 6:25:20 PM
Last modification on : Monday, February 11, 2019 - 4:22:53 PM

Links full text

Identifiers

Citation

Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, et al.. aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming. Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), Sep 2015, Lexington, United States. pp.112-126, ⟨10.1007/978-3-319-23264-5_10⟩. ⟨hal-01186996⟩

Share

Metrics

Record views

419