Answer Set Solving with Generalized Learned Constraints
Conflict learning plays a key role in modern Boolean constraint solving. Advanced in satisfiability testing, it has meanwhile become a base technology in many neighboring fields, among them answer set programming (ASP). However, learned constraints are only valid for a currently solved problem instance and do not carry over to similar instances. We address this issue in ASP and introduce a framework featuring an integrated feedback loop that allows for reusing conflict constraints. The idea is to extract (propositional) conflict constraints, generalize and validate them, and reuse them as integrity constraints. Although we explore our approach in the context of dynamic applications based on transition systems, it is driven by the ultimate objective of overcoming the issue that learned knowledge is bound to specific problem instances. We implemented this workflow in two systems, namely, a variant of the ASP solver clasp that extracts integrity constraints along with a downstream system for generalizing and validating them.
Answer Set Programming
Conflict Learning
Constraint Generalization
Generalized Constraint Feedback
9:1-9:15
Regular Paper
Martin
Gebser
Martin Gebser
Roland
Kaminski
Roland Kaminski
Benjamin
Kaufmann
Benjamin Kaufmann
Patrick
Lühne
Patrick Lühne
Javier
Romero
Javier Romero
Torsten
Schaub
Torsten Schaub
10.4230/OASIcs.ICLP.2016.9
M. Alviano, C. Dodaro, N. Leone, and F. Ricca. Advances in WASP. In F. Calimeri, G. Ianni, and M. Truszczyński, editors, Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), pages 40-54. Springer, 2015.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
G. Brewka, T. Eiter, and M. Truszczyński. Answer set programming at a glance. Communications of the ACM, 54(12):92-103, 2011.
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/
J. Charnley, S. Colton, and I. Miguel. Automated generation of implied constraints. In G. Brewka, S. Coradeschi, A. Perini, and P. Traverso, editors, Proceedings of the Seventeenth European Conference on Artificial Intelligence (ECAI'06), pages 73-77. IOS Press, 2006.
M. Dao-Tran, T. Eiter, M. Fink, G. Weidinger, and A. Weinzierl. OMiGA : An open minded grounding on-the-fly answer set solver. In L. Fariñas del Cerro, A. Herzig, and J. Mengin, editors, Proceedings of the Thirteenth European Conference on Logics in Artificial Intelligence (JELIA'12), pages 480-483. Springer, 2012.
B. De Cat and M. Bruynooghe. Detection and exploitation of functional dependencies for model generation. Theory and Practice of Logic Programming, 13(4-5):471-485, 2013.
R. Dechter. Constraint Processing. Morgan Kaufmann Publishers, 2003.
M. Gebser, R. Kaminski, B. Kaufmann, P. Lühne, J. Romero, and T. Schaub. Answer set solving with generalized learned constraints (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, M. Knecht, and T. Schaub. plasp: A prototype for PDDL-based planning in ASP. In J. Delgrande and W. Faber, editors, Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'11), pages 358-363. Springer, 2011.
M. Gebser, B. Kaufmann, and T. Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012.
M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Computing, 9:365-385, 1991.
E. Giunchiglia, Y. Lierler, and M. Maratea. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning, 36(4):345-377, 2006.
S. Haufe, S. Schiffel, and M. Thielscher. Automated verification of state sequence invariants in general game playing. Artificial Intelligence, 187-188:1-30, 2012.
M. Helmert. Concise finite-domain representations for PDDL planning tasks. Artificial Intelligence, 173(5-6):503-535, 2009.
M. Law, A. Russo, and K. Broda. Inductive learning of answer set programs. In E. Fermé and J. Leite, editors, Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA'14), pages 311-325. Springer, 2014.
V. Lifschitz. Answer set programming and plan generation. Artificial Intelligence, 138(1-2):39-54, 2002.
F. Lin. Discovering state invariants. In D. Dubois, C. Welty, and M. Williams, editors, Proceedings of the Ninth International Conference on Principles of Knowledge Representation and Reasoning (KR'04), pages 536-544. AAAI Press, 2004.
P. Lühne. Generalizing learned knowledge in answer set solving. Master’s thesis, Hasso Plattner Institute, Potsdam, 2015.
J. Marques-Silva and K. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999.
B. O'Sullivan. Automated modelling and solving in constraint programming. In M. Fox and D. Poole, editors, Proceedings of the Twenty-fourth National Conference on Artificial Intelligence (AAAI'10), pages 1493-1497. AAAI Press, 2010.
R. Otero. Induction of stable models. In C. Rouveirol and M. Sebag, editors, Proceedings of the Eleventh International Conference on Inductive Logic Programming (ILP'01), pages 193-205. Springer, 2001.
J. Rintanen. An iterative algorithm for synthesizing invariants. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI'00), pages 806-811. AAAI/MIT Press, 2000.
M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In W. Hunt and S. Johnson, editors, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD'00), pages 108-125. Springer, 2000.
Y. Vizel, G. Weissenbacher, and S. Malik. Boolean satisfiability solvers and their applications in model checking. Proceedings of the IEEE, 103(11):2021-2035, 2015.
A. Weinzierl. Learning non-ground rules for answer-set solving. In D. Pearce, S. Tasharrofi, E. Ternovska, and C. Vidal, editors, Proceedings of the Second Workshop on Grounding and Transformation for Theories with Variables (GTTV'13), pages 25-37, 2013.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode