×

zbMATH — the first resource for mathematics

Disjunctive answer set solvers via templates. (English) Zbl 1379.68046
Summary: 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 \(\Sigma^{\mathrm 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.
MSC:
68N17 Logic programming
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
Cmodels; Datalog; WASP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alviano, M.; Dodaro, C.; Faber, W.; Leone, N.; Ricca, F.; Cabalar, P.; Son, T. C., WASP: A native ASP solver based on constraint learning, Proc. of the 12th International Conference of Logic Programming and Nonmonotonic Reasoning (LPNMR 2013), 54-66, (2013), Springer: Springer, Berlin · Zbl 1272.68012
[2] Baral, C., Knowledge Representation, Reasoning and Declarative Problem Solving, (2003), Cambridge University Press · Zbl 1056.68139
[3] Brochenin, R.; Lierler, Y.; Maratea, M., (2014)
[4] Brooks, D. R.; Erdem, E.; Erdoğan, S. T.; Minett, J. W.; Ringe, D., Inferring phylogenetic trees using answer set programming, Journal of Automated Reasoning, 39, 471-511, (2007) · Zbl 1132.68676
[5] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Communications of the ACM, 5, 394-397, (1962) · Zbl 0217.54002
[6] Eiter, T.; Gottlob, G.; Miller, D., Proc. of the 1993 International Logic Programming Symposium (ILPS), Complexity results for disjunctive logic programming and application to nonmonotonic logics, 266-278, (1993), MIT Press
[7] Eiter, T.; Gottlob, G.; Mannila, H., Disjunctive datalog, ACM Transactions on Database Systems, 22, 364-418, (1997)
[8] Faber, W., (2002)
[9] Gebser, M.; Kaufmann, B.; Schaub, T.; Rossi, F., (2013)
[10] Gebser, M.; Schaub, T.; Etalle, S.; Truszczynski, M., Proc. of the 22nd International Conference on Logic Programming (ICLP 2006), Tableau calculi for answer set programming, 11-25, (2006), Springer: Springer, Berlin
[11] Gebser, M.; Schaub, T., Tableau calculi for logic programs under answer set semantics, ACM Transaction on Computational Logic, 14, 15, (2013) · Zbl 1353.68037
[12] Gelfond, M.; Lifschitz, V.; Kowalski, R.; Bowen, K., Proc. of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP 1988), The stable model semantics for logic programming, 1070-1080, (1988), MIT Press: MIT Press, Las Cruces
[13] Gelfond, M.; Lifschitz, V., Classical negation in logic programs and disjunctive databases, New Generation Computing, 9, 365-385, (1991) · Zbl 0735.68012
[14] Giunchiglia, E.; Leone, N.; Maratea, M., On the relation among answer set solvers, Annals of Mathematics and Artificial Intelligence, 53, 169-204, (2008) · Zbl 1165.68333
[15] Giunchiglia, E.; Maratea, M.; Gabbrielli, M.; Gupta, G., Proc. of the 21st International Conference on Logic Programming (ICLP 2005), On the relation between answer set and SAT procedures (or, between smodels and cmodels), 37-51, (2005), Springer: Springer, Berlin · Zbl 1165.68488
[16] Janhunen, T.; Niemelä, I.; Seipel, D.; Simons, P.; You, J.-H., Unfolding partiality and disjunctions in stable model semantics, ACM Transactions on Computunational Logic, 7, 1-37, (2006) · Zbl 1367.68035
[17] Koch, C.; Leone, N.; Pfeifer, G., Enhancing disjunctive logic programming systems by sat checkers, Artificial Intelligence, 151, 177-212, (2003) · Zbl 1082.68525
[18] Leone, N.; Faber, W.; Pfeifer, G.; Eiter, T.; Gottlob, G.; Perri, S.; Scarcello, F., The DLV system for knowledge representation and reasoning, ACM Transactions on Computational Logic, 7, 499-562, (2006) · Zbl 1367.68308
[19] Leone, N.; Rullo, P.; Scarcello, F., Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation, Information and Computation, 135, 69-112, (1997) · Zbl 0879.68019
[20] Lierler, Y.; Baral, C.; Greco, G.; Leone, N.; Terracina, G., Proc. of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2005), Cmodels: SAT-based disjunctive answer set solver, 447-452, (2005), Springer: Springer, Berlin · Zbl 1086.68002
[21] Lierler, Y.; De La Banda, M. G.; Pontelli, E., Proc. of the 24th International Conference on Logic Programming (ICLP 2008), Abstract answer set solvers, 377-391, (2008), Springer: Springer, Berlin
[22] Lierler, Y., (2010)
[23] Lierler, Y., Abstract answer set solvers with backjumping and learning, Theory and Practice of Logic Programming, 11, 135-169, (2011) · Zbl 1220.68038
[24] Lierler, Y.; Truszczynski, M., Transition systems for model generators - a unifying approach, Theory and Practice of Logic Programming, 11, 629-646, (2011) · Zbl 1222.68063
[25] Lifschitz, V., Proc. of the 16th International Conference on Logic Programming (ICLP 1999), Answer Set Planning, 23-37, (1999), The MIT Press: The MIT Press, Las Cruces
[26] Marek, V.; Truszczyński, M., The Logic Programming Paradigm: A 25-Year Perspective, Stable models and an alternative logic programming paradigm, 375-398, (1999), Springer-Verlag: Springer-Verlag, Berlin · Zbl 0979.68524
[27] Niemelä, I., Logic programs with stable model semantics as a constraint programming paradigm, Annals of Mathematics and Artificial Intelligence, 25, 241-273, (1999) · Zbl 0940.68018
[28] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), Journal of the ACM, 53, 937-977, (2006) · Zbl 1326.68164
[29] Perri, S.; Scarcello, F.; Catalano, G.; Leone, N., Enhancing DLV instantiator by backjumping techniques, Annals of Mathematics and Artificial Intelligence, 51, 195-228, (2007) · Zbl 1138.68019
[30] Ricca, F.; Grasso, G.; Alviano, M.; Manna, M.; Lio, V.; Iiritano, S.; Leone, N., Team-building with answer set programming in the gioia-tauro seaport, Theory and Practice of Logic Programming, 12, 361-381, (2012) · Zbl 1250.90050
[31] Simons, P.; Niemelä, I.; Soininen, T., Extending and implementing the stable model semantics, Artificial Intelligence, 138, 181-234, (2002) · Zbl 0995.68021
[32] Soininen, T.; Niemelä, I.; Gupta, G., Proc. of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL 1999), Developing a Declarative Rule Language for Applications in Product Configuration, 305-319, (1999), Springer: Springer, Berlin
[33] Syrjänen, T.; Eiter, T.; Faber, W.; Truszczynski, M., Proc. of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2001), Omega-restricted logic programs, 267-279, (2001), Springer: Springer, Berlin
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.