zbMATH — the first resource for mathematics

Abstract solvers for computing cautious consequences of ASP programs. (English) Zbl 1434.68066
Summary: Abstract solvers are a method to formally analyze algorithms that have been profitably used for describing, comparing and composing solving techniques in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP.
In this paper, we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers for cautious reasoning in ASP with new techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. By doing so, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. We implement some of the new solutions in the ASP solver \small WASP and show that their performance are comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions.
68N17 Logic programming
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Datalog; WASP
Full Text: DOI
[1] Alviano, M., Amendola, G., Dodaro, C., Leone, N., Maratea, M., and Ricca, F.2019. Evaluation of disjunctive programs in WASP. In Proc. of the 15th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2019), M.Balduccini, Y.Lierler, and S.Woltran, Eds. Lecture Notes in Computer Science, vol. 11481. Springer, 241-255. · Zbl 07115978
[2] Alviano, M. and Dodaro, C.2016. Anytime answer set optimization via unsatisfiable core shrinking. Theory and Practice of Logic Programming 16, 5-6, 533-551. · Zbl 1379.68033
[3] Alviano, M., Dodaro, C., Järvisalo, M., Maratea, M., and Previti, A.2018. Cautious reasoning in ASP via minimal models and unsatisfiable cores. Theory and Practice of Logic Programming 18, 3-4, 319-336. · Zbl 1451.68267
[4] Alviano, M., Dodaro, C., Leone, N., and Ricca, F.2015. Advances in WASP. In Proceedings of the 13th International Conference of Logic Programming and Nonmonotonic Reasoning (LPNMR 2015), F.Calimeri, G.Ianni, and M.Truszczynski, Eds. Lecture Notes in Computer Science, vol. 9345. Springer, 40-54. · Zbl 06504220
[5] Alviano, M., Dodaro, C., and Ricca, F.2014. Anytime computation of cautious consequences in answer set programming. Theory and Practice of Logic Programming 14, 4-5, 755-770. · Zbl 1307.68012
[6] Arenas, M., Bertossi, L. E., and Chomicki, J.2003. Answer sets for consistent query answering in inconsistent databases. Theory and Practice of Logic Programming 3, 4-5, 393-424. · Zbl 1079.68026
[7] Baral, C.2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press. · Zbl 1056.68139
[8] Brewka, G. and Eiter, T.2007. Equilibria in heterogeneous nonmonotonic multi-context systems. In Proceedings of National conference on Artificial Intelligence (AAAI 2007), AAAI Press, 385-390.
[9] Brochenin, R., Lierler, Y., and Maratea, M.2014. Abstract disjunctive answer set solvers. In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI 2014), Frontiers in Artificial Intelligence and Applications, vol. 263. IOS Press, 165-170. · Zbl 1366.68016
[10] Brochenin, R., Linsbichler, T., Maratea, M., Wallner, J. P., and Woltran, S.2018. Abstract solvers for Dung’s argumentation frameworks. Argument & Computation 9, 1, 41-72. · Zbl 1335.68246
[11] Brochenin, R. and Maratea, M.2015a. Abstract answer set solvers for cautious reasoning. In Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), M. D.Vos, T.Eiter, Y.Lierler, and F.Toni, Eds. CEUR Workshop Proceedings. vol. 1433. CEUR-WS.org. · Zbl 1407.68077
[12] Brochenin, R. and Maratea, M.2015b. Abstract solvers for quantified boolean formulas and their applications. In Proc. of AI*IA 2015: Advances in Artificial Intelligence - XIVth International Conference of the Italian Association for Artificial Intelligence, M.Gavanelli, E.Lamma, and F.Riguzzi, Eds. Lecture Notes in Computer Science, vol. 9336. Springer, 205-217. · Zbl 1407.68077
[13] Calimeri, F., Gebser, M., Maratea, M., and Ricca, F.2016. Design and results of the Fifth Answer Set Programming Competition. Artificial Intelligence 231, 151-181. · Zbl 1344.68042
[14] Calimeri, F., Ianni, G., and Ricca, F.2014. The third open answer set programming competition. Theory and Practice of Logic Programming 14, 1, 117-135.
[15] Di Rosa, E., Giunchiglia, E., and Maratea, M.2010. Solving satisfiability problems with preferences. Constraints 15, 4, 485-515. · Zbl 1208.68199
[16] Eiter, T.2005. Data integration and answer set programming. In Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2005), C.Baral, G.Greco, N.Leone, and G.Terracina, Eds. Lecture Notes in Computer Science, vol. 3662. Springer, 13-25. · Zbl 1152.68639
[17] Eiter, T., Gottlob, G., and Mannila, H.1997. Disjunctive Datalog. ACM Transactions on Database Systems 22, 3 (Sept.), 364-418.
[18] Eiter, T., Ianni, G., Lukasiewicz, T., Schindlauer, R., and Tompits, H.2008. Combining answer set programming with description logics for the semantic web. Artificial Intelligence 172, 12-13, 1495-1539. · Zbl 1183.68595
[19] Gebser, M., Kaufmann, B., and Schaub, T.2012. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence 187, 52-89. · Zbl 1251.68060
[20] Gebser, M., Maratea, M., and Ricca, F.2017. The sixth answer set programming competition. Journal of Artificial Intelligence Research 60, 41-95. · Zbl 1418.68030
[21] Gelfond, M. and Lifschitz, V.1988. The Stable Model Semantics for Logic Programming. In Proceedings of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP 1988). MIT Press, Cambridge, Mass., pp. 1070-1080.
[22] Gelfond, M. and Lifschitz, V.1991. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365-385. · Zbl 0735.68012
[23] Giunchiglia, E., Leone, N., and Maratea, M.2008. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence 53, 1-4, 169-204. · Zbl 1165.68333
[24] Giunchiglia, E., Maratea, M., and Tacchella, A.2002. Dependent and independent variables in propositional satisfiability. In Proc. of the European Conference on Logics in Artificial Intelligence (JELIA 2002), S.Flesca, S.Greco, N.Leone, and G.Ianni, Eds. Lecture Notes, vol. 2424. Springer, 296-307. · Zbl 1014.68528
[25] Giunchiglia, E., Maratea, M., and Tacchella, A.2003. (in)effectiveness of look-ahead techniques in a modern SAT solver. In Proc. of the 9th International Conference on Principles and Practice of Constraint Programming (CP 2003), F.Rossi, Ed. Lecture Notes in Computer Science, vol. 2833. Springer, 842-846.
[26] Janota, M., Lynce, I., and Marques-Silva, J.2015. Algorithms for computing backbones of propositional formulae. AI Communications 28, 2, 161-177. · Zbl 1373.68379
[27] Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., and Scarcello, F.2006. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic 7, 3, 499-562. · Zbl 1367.68308
[28] Lierler, Y.2008. Abstract answer set solvers. In Proceedings of the 24th International Conference on Logic Programming (ICLP 2008), M. G.de la Banda and E.Pontelli, Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 377-391. · Zbl 1185.68165
[29] Lierler, Y.2011. Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming 11, 135-169. · Zbl 1220.68038
[30] Lierler, Y.2014. Relating constraint answer set programming languages and algorithms. Artificial Intelligence 207, 1-22. · Zbl 1334.68041
[31] Lierler, Y. and Truszczynski, M.2011. Transition systems for model generators — a unifying approach. Theory and Practice of Logic Programming 11, 4-5, 629-646. · Zbl 1222.68063
[32] Lierler, Y. and Truszczynski, M.2013. Modular answer set solving. In Late-Breaking Developments in the Field of Artificial Intelligence. AAAI Workshops, vol. WS-13-17. AAAI. · Zbl 1357.68230
[33] Lierler, Y. and Truszczynski, M.2014. Abstract modular inference systems and solvers. In Proceedings of the 16th International Symposium on Practical Aspects of Declarative Languages (PADL 2014), M.Flatt and H.Guo, Eds. Lecture Notes in Computer Science, vol. 8324. Springer, 49-64. · Zbl 1357.68230
[34] Lierler, Y. and Truszczynski, M.2015. An abstract view on modularity in knowledge representation. In Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI 2015), B.Bonet and S.Koenig, Eds. AAAI Press, 1532-1538.
[35] Lierler, Y. and Truszczynski, M.2016. On abstract modular inference systems and solvers. Artificial Intelligence 236, 65-89. · Zbl 1357.68230
[36] Lynce, I. and Silva, J. P. M.2004. On computing minimum unsatisfiable cores. In Proc. of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004).
[37] Manna, M., Ricca, F., and Terracina, G.2013. Consistent query answering via ASP from different perspectives: Theory and practice. Theory and Practica of Logic Programming 13, 2, 227-252. · Zbl 1267.68082
[38] Marek, V. W. and Truszczyński, M.1998. Stable models and an alternative logic programming paradigm. CoRR cs.LO/9809032. · Zbl 0979.68524
[39] Niemelä, I.1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241-273. · Zbl 0940.68018
[40] Nieuwenhuis, R., Oliveras, A., and Tinelli, C.2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM53(6), 937-977. · Zbl 1326.68164
[41] Sebastiani, R.2007. Lazy satisability modulo theories. Journal fo Satisfiability, Boolean Modeling and Computation 3, 3-4, 141-224. · Zbl 1145.68501
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.