Answer Set Programming Modulo Acyclicity

• Autorzy: Bomanson J. , Janhunen T. , Schaub T. , Gebser M. , Kaufmann B.

Identyfikatory

DOI

10.3233/FI-2016-1398

• Konferencja: ASPOCP 2015 : ASPOCP International Workshop on “Answer Set Programming and Other Computing Paradigms” (8: August 31, 2015: Cork, Ireland)
• Języki publikacji: EN

Abstrakty

EN

Acyclicity constraints are prevalent in knowledge representation and applications where acyclic data structures such as DAGs and trees play a role. Recently, such constraints have been considered in the satisfiability modulo theories (SMT) framework, and in this paper we carry out an analogous extension to the answer set programming (ASP) paradigm. The resulting formalism, ASP modulo acyclicity, offers a rich set of primitives to express constraints related to recursive structures. In the technical results of the paper, we relate the new generalization with standard ASP by showing (i) how acyclicity extensions translate into normal rules, (ii) how weight constraint programs can be instrumented by acyclicity extensions to capture stability in analogy to unfounded set checking, and (iii) how the gap between supported and stable models is effectively closed in the presence of such an extension. Moreover, we present an efficient implementation of acyclicity constraints by incorporating a respective propagator into the stateof- the-art ASP solver CLASP. The implementation provides a unique combination of traditional unfounded set checking with acyclicity propagation. In the experimental part, we evaluate the interplay of these orthogonal checks by equipping logic programs with supplementary acyclicity constraints. The performance results show that native support for acyclicity constraints is a worthwhile addition, furnishing a complementary modeling construct in ASP itself as well as effective means for translation-based ASP solving.

Słowa kluczowe

EN

logic programming; knowledge representation; constraint satisfaction; performance evaluation; computer algorithms

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 147, nr 1
• Strony: 63--91
• Opis fizyczny: Bibliogr. 43 poz., rys., tab., wykr.

Twórcy

autor

Bomanson J.

• Aalto University, HIIT, Finland

autor

Janhunen T.

• Aalto University, HIIT, Finland

autor

Schaub T.

• University of Potsdam, Germany
• INRIA Rennes

autor

Gebser M.

• University of Potsdam, Germany

autor

Kaufmann B.

• University of Potsdam, Germany

Bibliografia

• [1] Bomanson J, Gebser M, Janhunen T, Kaufmann B, Schaub T. Answer Set Programming Modulo Acyclicity. In: Inclezan D, Maratea M, editors. Proceedings of the Eighth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP’15); 2015. Available from: https://sites.google.com/site/aspocp2015/ASPOCP2015paper5.pdf.
• [2] Bomanson J, Gebser M, Janhunen T, Kaufmann B, Schaub T. Answer Set Programming Modulo Acyclicity. In: Calimeri F, Ianni G, Truszczyński M, editors. Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’15). Springer-Verlag; 2015. p. 143–150. doi:10.1007/978-3-319-23264-5_13.
• [3] Cussens J. Bayesian Network Learning with Cutting Planes. In: Cozman F, Pfeffer A, editors. Proceedings of the Twenty-seventh International Conference on Uncertainty in Artificial Intelligence (UAI’11). AUAI Press; 2011. p. 153–160. Available from: https://dslpitt.org/papers/11/p153-cussens.pdf.
• [4] Corander J, Janhunen T, Rintanen J, Nyman H, Pensar J. Learning Chordal Markov Networks by Constraint Satisfaction. In: Burges C, Bottou L, Ghahramani Z, Weinberger K, editors. Proceedings of the Twenty-seventh Annual Conference on Neural Information Processing Systems (NIPS’13). Neural Information Processing Systems Foundation; 2013. p. 1349–1357. Available from: http://papers.nips.cc/paper/4960-learning-chordal-markov-networks-by-constraint-satisfaction.pdf.
• [5] Janhunen T, Gebser M, Rintanen J, Nyman H, Pensar J, Corander J. Learning Discrete Decomposable Graphical Models via Constraint Optimization. Statistics and Computing. 2015;advance access. doi:10.1007/s11222-015-9611-4.
• [6] Erdem E, Lifschitz V, Wong M. Wire Routing and Satisfiability Planning. In: Lloyd J, Dahl V, Furbach U, Kerber M, Lau K, Palamidessi C, Pereira L, Sagiv Y, Stuckey P, editors. Proceedings of the First International Conference on Computational Logic (CL’00). Springer-Verlag; 2000. p. 822–836. doi:10.1007/3-540-44957-4_55.
• [7] Koponen L, Oikarinen E, Janhunen T, Säilä L. Optimizing Phylogenetic Supertrees using Answer Set Programming. Theory and Practice of Logic Programming. 2015;15(4-5):604–619. doi:10.1017/S1471068415000265.
• [8] Barrett C, Sebastiani R, Seshia S, Tinelli C. Satisfiability Modulo Theories. In: Biere A, Heule M, van Maaren H, Walsh T, editors. Handbook of Satisfiability. IOS Press; 2009. p. 825–885. doi:10.3233/978-1-58603-929-5-825.
• [9] Biere A, Heule M, van Maaren H, Walsh T, editors. Handbook of Satisfiability. IOS Press; 2009. Available from: http://ebooks.iospress.nl/volume/handbook-of-satisfiability.
• [10] Gebser M, Janhunen T, Rintanen J. SAT Modulo Graphs: Acyclicity. In: Fermé E, Leite J, editors. Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA’14). Springer-Verlag; 2014. p. 137–151. doi:10.1007/978-3-319-11558-0_10.
• [11] Bayless S, Bayless N, Hoos H, Hu A. SAT Modulo Monotonic Theories. In: Bonet B, Koenig S, editors. Proceedings of the Twenty-Ninth National Conference on Artificial Intelligence (AAAI’15). AAAI Press; 2015. p. 3702–3709. Available from: http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9951.
• [12] Gebser M, Janhunen T, Rintanen J. Answer Set Programming as SAT Modulo Acyclicity. In: Schaub T, Friedrich G, O’Sullivan B, editors. Proceedings of the Twenty-first European Conference on Artificial Intelligence (ECAI’14). IOS Press; 2014. p. 351–356. doi:10.3233/978-1-61499-419-0-351.
• [13] Eén N, Sörensson N. An Extensible SAT-solver. In: Giunchiglia E, Tacchella A, editors. Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT’03). Springer-Verlag; 2004. p. 502–518. doi:10.1007/978-3-540-24605-3_37.
• [14] Audemard G, Simon L. Predicting Learnt Clauses Quality in Modern SAT Solvers. In: Boutilier C, editor. Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09). AAAI/MIT Press; 2009. p. 399–404. Available from: http://ijcai.org/Proceedings/09/Papers/074.pdf.
• [15] Baral C. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press; 2003. doi:10.1017/CBO9780511543357.
• [16] Simons P, Niemelä I, Soininen T. Extending and Implementing the Stable Model Semantics. Artificial Intelligence. 2002;138(1-2):181–234. doi:10.1016/S0004-3702(02)00187-X.
• [17] Gebser M, Kaufmann B, Schaub T. Conflict-Driven Answer Set Solving: From Theory to Practice. Artificial Intelligence. 2012;187-188:52–89. doi:10.1016/j.artint.2012.04.001.
• [18] Van Gelder A, Ross K, Schlipf J. The Well-Founded Semantics for General Logic Programs. Journal of the ACM. 1991;38(3):620–650. doi:10.1145/116825.116838.
• [19] Oikarinen E, Janhunen T. Achieving Compositionality of the Stable Model Semantics for smodels Programs. Theory and Practice of Logic Programming. 2008;8(5-6):717–761. doi: 10.1017/S147106840800358X.
• [20] Lifschitz V, Turner H. Splitting a Logic Program. In: Van Hentenryck P, editor. Proceedings of the Eleventh International Conference on Logic Programming (ICLP’94). MIT Press; 1994. p. 23–37. Available from: https://www.d.umn.edu/˜hudson/papers/iclp94a.pdf.
• [21] Gebser M, Kaminski R, Kaufmann B, Ostrowski M, Schaub T, Schneider M. Potassco: The Potsdam Answer Set Solving Collection. AI Communications. 2011;24(2):107–124. doi:10.3233/AIC-2011-0491.
• [22] Gebser M, Janhunen T, Rintanen J. ASP Encodings of Acyclicity Properties. In: Baral C, De Giacomo G, Eiter T, editors. Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’14). AAAI Press; 2014. Available from: http://www.aaai.org/ocs/index.php/KR/KR14/paper/view/8025.
• [23] Janhunen T. Some (In)translatability Results for Normal Logic Programs and Propositional Theories. Journal of Applied Non-Classical Logics. 2006;16(1-2):35–86. doi:10.3166/jancl.16.35-86.
• [24] Niemelä I. Stable Models and Difference Logic. Annals of Mathematics and Artificial Intelligence. 2008;53(1-4):313–329. doi:10.1007/s10472-009-9118-9.
• [25] Fages F. Consistency of Clark’s Completion and the Existence of Stable Models. Journal of Methods of Logic in Computer Science. 1994;1:51–60. Available from: http://lifeware.inria.fr/˜fages/Papers/MLCS.ps.gz.
• [26] Erdem E, Lifschitz V. Tight Logic Programs. Theory and Practice of Logic Programming. 2003;3(4-5):499–518. doi:10.1017/S1471068403001765.
• [27] Clark K. Negation as Failure. In: Gallaire H, Minker J, editors. Logic and Data Bases. Plenum Press; 1978. p. 293–322. doi:10.1007/978-1-4684-3384-5_11.
• [28] Soh T, Le Berre D, Roussel S, Banbara M, Tamura N. Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem. In: Fermé E, Leite J, editors. Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA’14). Springer-Verlag; 2014. p. 684–693. doi:10.1007/978-3-319-11558-0_52.
• [29] Alviano M, Calimeri F, Charwat G, Dao-Tran M, Dodaro C, Ianni G, Krennwallner T, Kronegger M, Oetsch J, Pfandler A, Pührer J, Redl C, Ricca F, Schneider P, Schwengerer M, Spendier L, Wallner J, Xiao G. The Fourth Answer Set Programming Competition: Preliminary Report. In: Cabalar P, Son T, editors. Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’13). Springer-Verlag; 2013. p. 42–53. doi:10.1007/978-3-642-40564-8_5.
• [30] Janhunen T, Niemelä I, Sevalnev M. Computing Stable Models via Reductions to Difference Logic. In: Erdem E, Lin F, Schaub T, editors. Proceedings of the Tenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’09). Springer-Verlag; 2009. p. 142–154. doi:10.1007/978-3-642-04238-6_14.
• [31] Bomanson J, Janhunen T. Normalizing Cardinality Rules using Merging and Sorting Constructions. In: Cabalar P, Son T, editors. Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’13). Springer-Verlag; 2013. p. 187–199. doi:10.1007/978-3-642-40564-8_19.
• [32] Alviano M, Dodaro C, Leone N, Ricca F. Advances in WASP. In: Calimeri F, Ianni G, Truszczyński M, editors. Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’15). Springer-Verlag; 2015. p. 40–54. doi:10.1007/978-3-319-23264-5_5.
• [33] Gebser M, Ostrowski M, Schaub T. Constraint Answer Set Solving. In: Hill P, Warren D, editors. Proceedings of the Twenty-fifth International Conference on Logic Programming (ICLP’09). Springer-Verlag; 2009. p. 235–249. doi:10.1007/978-3-642-02846-5_22.
• [34] Liu G, Janhunen T, Niemelä I. Answer Set Programming via Mixed Integer Programming. In: Brewka G, Eiter T, McIlraith S, editors. Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’12). AAAI Press; 2012. p. 32–42. Available from: http://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4516.
• [35] Lee J, Meng Y. Answer Set Programming Modulo Theories and Reasoning about Continuous Changes. In: Rossi F, editor. Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI’13). IJCAI/AAAI Press; 2013. p. 990–996. Available from: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6895.
• [36] Eiter T, Ianni G, Schindlauer R, Tompits H. DLVHEX: A Prover for Semantic-Web Reasoning under the Answer-Set Semantics. In: Proceedings of the International Conference on Web Intelligence (WI’06). IEEE Computer Society; 2006. p. 1073–1074. doi:10.1109/WI.2006.64.
• [37] Mellarkod V, Gelfond M, Zhang Y. Integrating Answer Set Programming and Constraint Logic Programming. Annals of Mathematics and Artificial Intelligence. 2008;53(1-4):251–287. doi:10.1007/s10472-009-9116-y.
• [38] Lierler Y. Relating Constraint Answer Set Programming Languages and Algorithms. Artificial Intelligence. 2014;207:1–22. doi:10.1016/j.artint.2013.10.004.
• [39] Gebser M, Kaufmann B, Schaub T. Solution Enumeration for Projected Boolean Search Problems. In: van Hoeve W, Hooker J, editors. Proceedings of the Sixth International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR’09). Springer-Verlag; 2009. p. 71–86. doi:10.1007/978-3-642-01929-6_7.
• [40] Gebser M, Schaub T. Tableau Calculi for Logic Programs under Answer Set Semantics. ACM Transactions on Computational Logic. 2013;14(2):15:1–15:40. doi:10.1145/2480759.2480767.
• [41] Chen X, Ji J, Lin F. Computing Loops With at Most One External Support Rule. In: Brewka G, Lang J, editors. Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning (KR’08). AAAI Press; 2008. p. 401–410. Available from: http://www.aaai.org/Library/KR/2008/kr08-039.php.
• [42] Drescher C, Walsh T. Efficient Approximation of Well-Founded Justification and Well-Founded Domination. In: Cabalar P, Son T, editors. Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’13). Springer-Verlag; 2013. p. 277–289. doi:10.1007/978-3-642-40564-8_28.
• [43] Nguyen M, Janhunen T, Niemelä I. Translating Answer-Set Programs into Bit-Vector Logic. In: Tompits H, Abreu S, Oetsch J, Pührer J, Seipel D, Umeda M, Wolf A, editors. Proceedings of the Nineteenth International Conference on Applications of Declarative Programming and Knowledge Management (INAP’11) and the Twenty-fifth Workshop on Logic Programming (WLP’11). Springer-Verlag; 2013. p. 105–116. doi:10.1007/978-3-642-41524-1_6.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).