Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming
This work provides a flexible, first-order encoding method for CSPs, which is incremental as it builds upon existing systems like sugar for parsing and normalization.
The authors tackled the problem of solving finite linear constraint satisfaction problems (CSPs) by developing an alternative approach using Answer Set Programming (ASP) instead of SAT solvers, resulting in the aspartame system that is empirically competitive with the award-winning sugar system.
Encoding finite linear CSPs as Boolean formulas and solving them by using modern SAT solvers has proven to be highly effective, as exemplified by the award-winning sugar system. We here develop an alternative approach based on ASP. This allows us to use first-order encodings providing us with a high degree of flexibility for easy experimentation with different implementations. 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.