Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-13T00:54:50.040Z Has data issue: false hasContentIssue false
  • English
  • Français

Disjunctive answer set solvers via templates

Published online by Cambridge University Press:  17 December 2015

REMI BROCHENIN ,
MARCO MARATEA  and
YULIYA LIERLER
REMI BROCHENIN
Affiliation:
DIBRIS, University of Genova, Viale F. Causa 15, 16145, Genova, Italy (e-mail: [email protected], [email protected])
MARCO MARATEA
Affiliation:
DIBRIS, University of Genova, Viale F. Causa 15, 16145, Genova, Italy (e-mail: [email protected], [email protected])
YULIYA LIERLER
Affiliation:
Department of Computer Science, University of Nebraska at Omaha, 6001 Dodge Street, Omaha, NE 68182 (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is ΣP 2-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely dlv, gnt, cmodels, clasp and wasp. In this paper, we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers dlv, gnt, and cmodels. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers.

Keywords

answer set programmingabstract solvers
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 16 , Issue 4 , July 2016 , pp. 465 - 497
Copyright
Copyright © Cambridge University Press 2015 

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., Dodaro, C., Faber, W., Leone, N. and Ricca, F. 2013. WASP: A native ASP solver based on constraint learning. In Proc. of the 12th International Conference of Logic Programming and Nonmonotonic Reasoning (LPNMR 2013), Cabalar, P. and Son, T. C., Eds. Lecture Notes in Computer Science, vol. 8148. Springer, Berlin, 54–66.Google Scholar
Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.Google Scholar
Brochenin, R., Lierler, Y. and Maratea, M. 2014. Abstract disjunctive answer set solvers. In Proc. of the 21st European Conference on Artificial Intelligence (ECAI 2014). Frontiers in Artificial Intelligence and Applications, vol. 263. IOS, Amsterdam, 165–170.Google Scholar
Brooks, D. R., Erdem, E., Erdoğan, S. T., Minett, J. W. and Ringe, D. 2007. Inferring phylogenetic trees using answer set programming. Journal of Automated Reasoning 39, 471–511.Google Scholar
Davis, M., Logemann, G. and Loveland, D. 1962. A machine program for theorem proving. Communications of the ACM 5 (7), 394–397.Google Scholar
Eiter, T. and Gottlob, G. 1993. Complexity results for disjunctive logic programming and application to nonmonotonic logics. In Proc. of the 1993 International Logic Programming Symposium (ILPS), Miller, D., Ed. MIT Press, 266–278.Google Scholar
Eiter, T., Gottlob, G. and Mannila, H. 1997. Disjunctive datalog. ACM Transactions on Database Systems 22 (3), 364–418.Google Scholar
Faber, W. 2002. Enhancing Efficiency and Expressiveness in Answer Set Programming Systems. Ph.D. thesis, Vienna University of Technology.Google Scholar
Gebser, M., Kaufmann, B. and Schaub, T. 2013. Advanced conflict-driven disjunctive answer set solving. In Proc. of the 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), Rossi, F., Ed. IJCAI/AAAI.Google Scholar
Gebser, M. and Schaub, T. 2006. Tableau calculi for answer set programming. In Proc. of the 22nd International Conference on Logic Programming (ICLP 2006), Etalle, S. and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 4079. Springer, Berlin, 11–25.Google Scholar
Gebser, M. and Schaub, T. 2013. Tableau calculi for logic programs under answer set semantics. ACM Transaction on Computational Logic 14 (2), 15.Google Scholar
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proc. of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP 1988), Kowalski, R. and Bowen, K., Eds. MIT Press, Las Cruces, 1070–1080.Google Scholar
Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 365–385.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), 169–204.Google Scholar
Giunchiglia, E. and Maratea, M. 2005. On the relation between answer set and SAT procedures (or, between smodels and cmodels). In Proc. of the 21st International Conference on Logic Programming (ICLP 2005), Gabbrielli, M. and Gupta, G., Eds. Lecture Notes in Computer Science, vol. 3668. Springer, Berlin, 37–51.Google Scholar
Janhunen, T., Niemelä, I., Seipel, D., Simons, P. and You, J.-H. 2006. Unfolding partiality and disjunctions in stable model semantics. ACM Transactions on Computunational Logic 7 (1), 1–37.Google Scholar
Koch, C., Leone, N. and Pfeifer, G. 2003. Enhancing disjunctive logic programming systems by sat checkers. Artificial Intelligence 151 (1–2), 177–212.CrossRefGoogle Scholar
Leone, N., Faber, W., Pfeifer, G., 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.Google Scholar
Leone, N., Rullo, P. and Scarcello, F. 1997. Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Information and Computation 135 (2), 69–112.Google Scholar
Lierler, Y. 2005. Cmodels: SAT-based disjunctive answer set solver. In Proc. 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, Berlin, 447–452.Google Scholar
Lierler, Y. 2008. Abstract answer set solvers. In Proc. 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, Berlin, 377–391.Google Scholar
Lierler, Y. 2010. SAT-Based Answer Set Programming. Ph.D. thesis, University of Texas at Austin.Google Scholar
Lierler, Y. 2011. Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming 11, 135–169.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), 629–646.CrossRefGoogle Scholar
Lifschitz, V. 1999. Answer Set Planning. In Proc. of the 16th International Conference on Logic Programming (ICLP 1999), D. D. Schreye, Ed. The MIT Press, Las Cruces, 23–37.Google Scholar
Marek, V. and Truszczyński, M. 1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm: A 25-Year Perspective. Springer-Verlag, Berlin, 375–398.CrossRefGoogle Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273.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), 937–977.CrossRefGoogle Scholar
Perri, S., Scarcello, F., Catalano, G. and Leone, N. 2007. Enhancing DLV instantiator by backjumping techniques. Annals of Mathematics and Artificial Intelligence 51 (2–4), 195–228.Google Scholar
Ricca, F., Grasso, G., Alviano, M., Manna, M., Lio, V., Iiritano, S. and Leone, N. 2012. Team-building with answer set programming in the gioia-tauro seaport. Theory and Practice of Logic Programming 12 (3), 361–381.Google Scholar
Simons, P., Niemelä, I. and Soininen, T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence 138, 181–234.Google Scholar
Soininen, T. and Niemelä, I. 1999. Developing a Declarative Rule Language for Applications in Product Configuration. In Proc. of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL 1999), Gupta, G., Ed. Lecture Notes in Computer Science, vol. 1551. Springer, Berlin, 305–319.Google Scholar
Syrjänen, T. 2001. Omega-restricted logic programs. In Proc. of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2001), Eiter, T., Faber, W., and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 2173. Springer, Berlin, 267–279.Google Scholar