aspartame: solving constraint satisfaction problems with answer set programming

DOI10.1007/978-3-319-23264-5_10MaRDI QIDQ3449196zbMATH OpenOpenAlexFDO

Authors Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise

Publication date 4 November 2015

Published in Logic Programming and Nonmonotonic Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1312.6113

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic programming (68N17)

Abstract: 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.

Recommendations

• Representing constraint satisfaction problems in answer set programming
• A translational approach to constraint answer set solving
• Constraint Answer Set Solving
• ASP modulo CSP: the clingcon system
• Answer set programming based on propositional satisfiability

Cites work

• scientific article; zbMATH DE number 4162321 (Why is no real title available?)
• scientific article; zbMATH DE number 2080324 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A SAT-based method for solving the two-dimensional strip packing problem
• A translational approach to constraint answer set solving
• ASP modulo CSP: the clingcon system
• Another look at graph coloring via propositional satisfiability
• Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems
• Compiling finite domain constraints to SAT with BEE
• Compiling finite linear CSP into SAT
• Constraint Answer Set Solving
• Generating combinatorial test cases by efficient SAT encodings suitable for CDCL SAT solvers
• Handbook of constraint programming.
• Knowledge Representation, Reasoning and Declarative Problem Solving
• On the parallel complexity of discrete relaxation in constraint satisfaction networks
• Promoting robust black-box solvers through competitions
• Propagation via lazy clause generation
• Representing constraint satisfaction problems in answer set programming
• aspartame: solving constraint satisfaction problems with answer set programming

Cited in

(4)

• Evaluating ASP and commercial solvers on the CSPLib
• Clingo goes linear constraints over reals and integers
• aspartame: solving constraint satisfaction problems with answer set programming
• \textit{clingcon}: the next generation

Describes a project that uses

Uses Software

• Clingcon

This page was built for publication: aspartame: solving constraint satisfaction problems with answer set programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3449196)