Document Open Access Logo

Theory Solving Made Easy with Clingo 5

Authors Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, Philipp Wanko

PDF

File

Thumbnail PDF
PDF
OASIcs.ICLP.2016.2.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Answer Set Programming
  • Theory Language
  • Theory Propagation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, and Philipp Wanko. Theory Solving Made Easy with Clingo 5. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/OASIcs.ICLP.2016.2

Author Details

Martin Gebser
Roland Kaminski
Benjamin Kaufmann
Max Ostrowski
Torsten Schaub
Philipp Wanko

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. M. Banbara, B. Kaufmann, M. Ostrowski, and T. Schaub. Clingcon: The next generation. Submitted for publication, 2016. Google Scholar
  4. C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability modulo theories. In Biere et al. [7], pages 825-885. Google Scholar
  5. M. Bartholomew and J. Lee. System aspmt2smt: Computing ASPMT theories by SMT solvers. In Fermé and Leite [15], pages 529-542. Google Scholar
  6. R. Bellman. On a routing problem. Quarterly of Applied Mathematics, 16:87-90, 1958. Google Scholar
  7. A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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.
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. L. Ford and D. Fulkerson. Flows in networks. Princeton University Press, 1962. Google Scholar
  17. 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.
  18. 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.
  19. 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. Google Scholar
  20. M. Gebser, B. Kaufmann, and T. Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. J. Marques-Silva, I. Lynce, and S. Malik. Conflict-driven clause learning SAT solvers. In Biere et al. [7], pages 131-153. Google Scholar
  25. M. Ostrowski and T. Schaub. ASP modulo CSP: The clingcon system. Theory and Practice of Logic Programming, 12(4-5):485-503, 2012. Google Scholar
  26. P. Simons, I. Niemelä, and T. Soininen. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2):181-234, 2002. Google Scholar
  27. E. Taillard. Benchmarks for basic scheduling problems. European Journal of Operational Research, 64(2):278-285, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact