Abstract
Disjunctive Logic Programming (DLP) under the answer set semantics is an advanced formalism for knowledge representation and reasoning. It is generally considered more expressive than normal (disjunction-free) Logic Programming, whose expressiveness is limited to properties decidable in NP.
However, this higher expressiveness comes at a computational cost, and while there are several efficient systems for the normal case, we are only aware of few solid implementations for full DLP.
In this paper we investigate novel techniques to couple two main modules (a model generator and a model checker) commonly found in DLP systems more tightly. Instead of using the checker only as a boolean oracle, in our approach, upon a failed check it also returns a so-called unfounded set. Intuitively, this set explains why a model candidate is not an answer set, and the generator employs this knowledge to backtrack until that set is no longer unfounded, which is vastly more efficient than employing full-fledged model checks to control backtracking.
Furthermore, we invoke the checker not only for actual model candidates, but also on partial models during model generation to possibly prune the search space.
We implemented these approaches in DLV, a state-of-the-art implementation of DLP according to recent comparisons, and carried out experiments; tests on hard benchmark instances show a significant speedup of a factor of two and above.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Babovich, Y.: Cmodels homepage, http://www.cs.utexas.edu/users/tag/cmodels.html
Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2002)
Calimeri, F., Faber, W., Leone, N., Pfeifer, G.: Pruning Operators for Answer Set Programming Systems. In: NMR 2002, April 2002, pp. 200–209 (2002)
Dowling, W.F., Gallier, J.H.: Linear-time Algorithms for Testing the Satisfability of Propositional Horn Formulae. JLP 3, 267–284 (1984)
Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. JACM 7, 201–215 (1960)
Eiter, T., Faber, W., Leone, N., Pfeifer, G., Polleres, A.: A Logic Programming Approach to Knowledge-State Planning: Semantics and Complexity. To appear in ACM TOCL (2003)
Eiter, T., Gottlob, G.: On the Computational Cost of Disjunctive Logic Programming: Propositional Case. AMAI 15(3/4), 289–323 (1995)
Eiter, T., Gottlob, G., Mannila, H.: Disjunctive Datalog. ACM TODS 22(3), 364–418 (1997)
Eiter, T., Leone, N., Mateis, C., Pfeifer, G., Scarcello, F.: Progress Report on the Disjunctive Deductive Database System dlv. In: Andreasen, T., Christiansen, H., Larsen, H.L. (eds.) FQAS 1998. LNCS (LNAI), vol. 1495, pp. 148–163. Springer, Heidelberg (1998)
East, D., Truszczyński, M.: aspps – An Implementation of Answer-Set Programming with Propositional Schemata. In: Eiter, T., Faber, W., Truszczyński, M. (eds.) LPNMR 2001. LNCS (LNAI), vol. 2173, pp. 402–405. Springer, Heidelberg (2001)
Faber, W., Leone, N., Pfeifer, G.: Experimenting with Heuristics for Answer Set Programming. In: IJCAI 2001, pp. 635–640. Morgan Kaufmann, San Francisco (2001)
Faber, W., Pfeifer, G.: DLV homepage (since 1996), http://www.dlvsystem.com/
Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365–385 (1991)
Gent, I., Walsh, T.: The QSAT Phase Transition. In: AAAI (1999)
Janhunen, T., Niemelä, I., Seipel, D., Simons, P., You, J.-H.: Unfolding Partiality and Disjunctions in Stable Model Semantics. Tech. Report cs.AI/0303009, arXiv.org
Janhunen, T., Niemelä, I., Simons, P., You, J.-H.: Partiality and Disjunctions in Stable Model Semantics. In: KR 2000, April 12-15, pp. 411–419. Morgan Kaufmann, San Francisco (2000)
Koch, C., Leone, N., Pfeifer, G.: Using SAT Checkers for Disjunctive Logic Programming Systems. Artificial Intelligence (2003) (to appear)
Lifschitz, V.: Foundations of Logic Programming. In: Principles of Knowledge Representation, pp. 69–127. CSLI Publications, Stanford (1996)
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV System for Knowledge Representation and Reasoning. Tech. Report cs.AI/0211004, arXiv.org (November 2002) (submitted to ACM TOCL)
Leone, N., Rullo, P., Scarcello, F.: Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics and Computation. Information and Computation 135(2), 69–112
Leone, N., Rosati, R., Scarcello, F.: Enhancing Answer Set Planning. In: IJCAI 2001, Workshop on Planning under Uncertainty and Incomplete Information, pp. 33–42 (2001)
Lin, F., Zhao, Y.: ASSAT: Computing Answer Sets of a Logic Program by SAT Solvers. In: AAAI 2002. AAAI Press / MIT Press (2002)
McCain, N.: The Causal Calculator (1999), http://www.cs.utexas.edu/users/tag/cc/
Papadimitriou, C.: Computational Complexity. Addison-Wesley, Reading (1994)
Przymusinski, T.C.: Well-founded Semantics Coincides with Three-valued Stable Semantics. Fundamenta Informaticae 13, 445–464 (1990)
Simons, P.: Smodels Homepage (since 1996), http://www.tcs.hut.fi/Software/smodels/
Simons, P., Niemelä, I., Soininen, T.: Extending and Implementing the Stable Model Semantics. Artificial Intelligence 138, 181–234 (2002)
Syrjänen, T.: Lparse User’s Manual (2002), http://www.tcs.hut.fi/Software/smodels/
Zhao, Y.: ASSAT homepage, http://assat.cs.ust.hk/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pfeifer, G. (2003). Improving the Model Generation/Checking Interplay to Enhance the Evaluation of Disjunctive Programs. In: Lifschitz, V., Niemelä, I. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2004. Lecture Notes in Computer Science(), vol 2923. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24609-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-24609-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20721-4
Online ISBN: 978-3-540-24609-1
eBook Packages: Springer Book Archive