Hostname: page-component-cd9895bd7-7cvxr Total loading time: 0 Render date: 2024-12-23T12:09:12.941Z Has data issue: false hasContentIssue false

Abstract Solvers for Computing Cautious Consequences of ASP programs

Published online by Cambridge University Press:  20 September 2019

GIOVANNI AMENDOLA
Affiliation:
University of Calabria, Italy (e-mails: [email protected], [email protected])
CARMINE DODARO
Affiliation:
University of Calabria, Italy (e-mails: [email protected], [email protected])
MARCO MARATEA
Affiliation:
University of Genoa, Italy (e-mail: [email protected])

Abstract

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 wasp and show that their performance are comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions.

Type
Original Article
Copyright
© Cambridge University Press 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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), Balduccini, M., Lierler, Y., and Woltran, S., Eds. Lecture Notes in Computer Science, vol. 11481. Springer, 241255.CrossRefGoogle Scholar
Alviano, M. and Dodaro, C. 2016. Anytime answer set optimization via unsatisfiable core shrinking. Theory and Practice of Logic Programming 16, 5-6, 533551.Google Scholar
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, 319336.CrossRefGoogle Scholar
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), Calimeri, F., Ianni, G., and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 9345. Springer, 4054.Google Scholar
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, 755770.Google Scholar
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, 393424.Google Scholar
Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.Google Scholar
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, 385390.Google Scholar
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, 165170.Google Scholar
Brochenin, R., Linsbichler, T., Maratea, M., Wallner, J. P., and Woltran, S. 2018. Abstract solvers for Dung’s argumentation frameworks. Argument & Computation 9, 1, 4172.Google Scholar
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), Vos, M. D., Eiter, T., Lierler, Y., and Toni, F., Eds. CEUR Workshop Proceedings. vol. 1433. CEUR-WS.org.Google Scholar
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, Gavanelli, M., Lamma, E., and Riguzzi, F., Eds. Lecture Notes in Computer Science, vol. 9336. Springer, 205217.Google Scholar
Calimeri, F., Gebser, M., Maratea, M., and Ricca, F. 2016. Design and results of the Fifth Answer Set Programming Competition. Artificial Intelligence 231, 151181.Google Scholar
Calimeri, F., Ianni, G., and Ricca, F. 2014. The third open answer set programming competition. Theory and Practice of Logic Programming 14, 1, 117135.Google Scholar
Di Rosa, E., Giunchiglia, E., and Maratea, M. 2010. Solving satisfiability problems with preferences. Constraints 15, 4, 485515.Google Scholar
Eiter, T. 2005. Data integration and answer set programming. In Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2005), Baral, C., Greco, G., Leone, N., and Terracina, G., Eds. Lecture Notes in Computer Science, vol. 3662. Springer, 1325.CrossRefGoogle Scholar
Eiter, T., Gottlob, G., and Mannila, H. 1997. Disjunctive Datalog. ACM Transactions on Database Systems 22, 3 (Sept.), 364418.CrossRefGoogle Scholar
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, 14951539.CrossRefGoogle Scholar
Gebser, M., Kaufmann, B., and Schaub, T. 2012. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence 187, 5289.Google Scholar
Gebser, M., Maratea, M., and Ricca, F. 2017. The sixth answer set programming competition. Journal of Artificial Intelligence Research 60, 4195.Google Scholar
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. 10701080.Google Scholar
Gelfond, M. and Lifschitz, V. 1991. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365385.Google Scholar
Giunchiglia, E., Leone, N., and Maratea, M. 2008. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence 53, 1-4, 169204.Google Scholar
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), Flesca, S., Greco, S., Leone, N., and Ianni, G., Eds. Lecture Notes, vol. 2424. Springer, 296307.Google Scholar
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), Rossi, F., Ed. Lecture Notes in Computer Science, vol. 2833. Springer, 842846.CrossRefGoogle Scholar
Janota, M., Lynce, I., and Marques-Silva, J. 2015. Algorithms for computing backbones of propositional formulae. AI Communications 28, 2, 161177.Google Scholar
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, 499562.Google Scholar
Lierler, Y. 2008. Abstract answer set solvers. In Proceedings of the 24th International Conference on Logic Programming (ICLP 2008), de la Banda, M. G. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 377391.Google Scholar
Lierler, Y. 2011. Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming 11, 135169.Google Scholar
Lierler, Y. 2014. Relating constraint answer set programming languages and algorithms. Artificial Intelligence 207, 122.Google Scholar
Lierler, Y. and Truszczynski, M. 2011. Transition systems for model generators — a unifying approach. Theory and Practice of Logic Programming 11, 4-5, 629646.Google Scholar
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.Google Scholar
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), Flatt, M. and Guo, H., Eds. Lecture Notes in Computer Science, vol. 8324. Springer, 4964.Google Scholar
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), Bonet, B. and Koenig, S., Eds. AAAI Press, 15321538.Google Scholar
Lierler, Y. and Truszczynski, M. 2016. On abstract modular inference systems and solvers. Artificial Intelligence 236, 6589.Google Scholar
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).Google Scholar
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, 227252.Google Scholar
Marek, V. W. and Truszczyński, M. 1998. Stable models and an alternative logic programming paradigm. CoRR cs.LO/9809032.Google Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241273.Google Scholar
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 ACM 53(6), 937977.Google Scholar
Sebastiani, R. 2007. Lazy satisability modulo theories. Journal fo Satisfiability, Boolean Modeling and Computation 3, 3-4, 141224.Google Scholar
Supplementary material: PDF

Amendola et al. supplementary material

Online Appendix

Download Amendola et al. supplementary material(PDF)
PDF 189.3 KB