Theory Solving Made Easy with Clingo 5
Answer Set Programming (ASP) is a model, ground, and solve paradigm. The integration of application- or theory-specific reasoning into ASP systems thus impacts on many if not all elements of its workflow, viz. input language, grounding, intermediate language, solving, and output format. We address this challenge with the fifth generation of the ASP system clingo and its grounding and solving components by equipping them with well-defined generic interfaces facilitating the manifold integration efforts. On the grounder's side, we introduce a generic way of specifying language extensions and propose an intermediate format accommodating their ground representation. At the solver end, this is accompanied by high-level interfaces easing the integration of theory propagators dealing with these extensions.
Answer Set Programming
Theory Language
Theory Propagation
2:1-2:15
Regular Paper
Martin
Gebser
Martin Gebser
Roland
Kaminski
Roland Kaminski
Benjamin
Kaufmann
Benjamin Kaufmann
Max
Ostrowski
Max Ostrowski
Torsten
Schaub
Torsten Schaub
Philipp
Wanko
Philipp Wanko
10.4230/OASIcs.ICLP.2016.2
M. Abseher, B. Bliem, G. Charwat, F. Dusberger, M. Hecher, and S. Woltran. The D-FLAT system for dynamic programming on tree decompositions. In Fermé and Leite [15], pages 558-572.
M. Balduccini. Representing constraint satisfaction problems in answer set programming. In Proceedings of the Second Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP'09), pages 16-30, 2009.
M. Banbara, B. Kaufmann, M. Ostrowski, and T. Schaub. Clingcon: The next generation. Submitted for publication, 2016.
C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability modulo theories. In Biere et al. [7], pages 825-885.
M. Bartholomew and J. Lee. System aspmt2smt: Computing ASPMT theories by SMT solvers. In Fermé and Leite [15], pages 529-542.
R. Bellman. On a routing problem. Quarterly of Applied Mathematics, 16:87-90, 1958.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009.
J. Bomanson, M. Gebser, T. Janhunen, B. Kaufmann, and T. Schaub. Answer set programming modulo acyclicity. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), pages 143-150. Springer, 2015.
P. Cabalar, R. Kaminski, M. Ostrowski, and T. Schaub. An ASP semantics for default reasoning with constraints. In Proceedings of the Twenty-fifth International Joint Conference on Artificial Intelligence (IJCAI'16), pages 1015-1021. IJCAI/AAAI Press, 2016.
F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, F. Ricca, and T. Schaub. ASP-Core-2: Input language format. Available at https://www.mat.unical.it/aspcomp2013/ASPStandardization/, 2012.
https://www.mat.unical.it/aspcomp2013/ASPStandardization/
S. Cotton and O. Maler. Fast and flexible difference constraint propagation for DPLL(T). In Proceedings of the Ninth International Conference on Theory and Applications of Satisfiability Testing (SAT'06), pages 170-183. Springer, 2006.
C. Drescher and T. Walsh. Answer set solving with lazy nogood generation. In Technical Communications of the Twenty-eighth International Conference on Logic Programming (ICLP'12), pages 188-200. Leibniz International Proceedings in Informatics, 2012.
T. Eiter, E. Erdem, H. Erdogan, and M. Fink. Finding similar/diverse solutions in answer set programming. Theory and Practice of Logic Programming, 13(3):303-359, 2013.
T. Eiter, M. Fink, T. Krennwallner, and C. Redl. Conflict-driven ASP solving with external sources. Theory and Practice of Logic Programming, 12(4-5):659-679, 2012.
E. Fermé and J. Leite, editors. Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA'14), volume 8761 of Lecture Notes in Artificial Intelligence. Springer, 2014.
L. Ford and D. Fulkerson. Flows in networks. Princeton University Press, 1962.
M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, and P. Wanko. Theory solving made easy with clingo 5 (extended version). Available at http://www.cs.uni-potsdam.de/wv/publications/, 2016.
http://www.cs.uni-potsdam.de/wv/publications/
M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Clingo = ASP + control: Preliminary report. In Technical Communications of the Thirtieth International Conference on Logic Programming (ICLP'14), 2014. Available at URL: http://arxiv.org/abs/1405.3694.
http://arxiv.org/abs/1405.3694
M. Gebser, B. Kaufmann, R. Otero, J. Romero, T. Schaub, and P. Wanko. Domain-specific heuristics in answer set programming. In Proceedings of the Twenty-Seventh National Conference on Artificial Intelligence (AAAI'13), pages 350-356. AAAI Press, 2013.
M. Gebser, B. Kaufmann, and T. Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012.
T. Janhunen, G. Liu, and I. Niemelä. Tight integration of non-ground answer set programming and satisfiability modulo theories. In Proceedings of the First Workshop on Grounding and Transformation for Theories with Variables (GTTV'11), pages 1-13, 2011.
V. Lifschitz. What is answer set programming? In Proceedings of the Twenty-third National Conference on Artificial Intelligence (AAAI'08), pages 1594-1597. AAAI Press, 2008.
G. Liu, T. Janhunen, and I. Niemelä. Answer set programming via mixed integer programming. In Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (KR'12), pages 32-42. AAAI Press, 2012.
J. Marques-Silva, I. Lynce, and S. Malik. Conflict-driven clause learning SAT solvers. In Biere et al. [7], pages 131-153.
M. Ostrowski and T. Schaub. ASP modulo CSP: The clingcon system. Theory and Practice of Logic Programming, 12(4-5):485-503, 2012.
P. Simons, I. Niemelä, and T. Soininen. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2):181-234, 2002.
E. Taillard. Benchmarks for basic scheduling problems. European Journal of Operational Research, 64(2):278-285, 1993.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode