Abstract
Many real-world applications, like planning or model checking, comprise a parameter reflecting the size of a solution. In a propositional formalism like Answer Set Programming (ASP), such problems can only be dealt with in a bounded way, considering one problem instance after another by gradually increasing the bound on the solution size. We thus propose an incremental approach to both grounding and solving in ASP. Our goal is to avoid redundancy by gradually processing the extensions to a problem rather than repeatedly re-processing the entire (extended) problem. We start by furnishing a formal framework capturing our incremental approach in terms of module theory. In turn, we take advantage of this framework for guiding the successive treatment of program slices during grounding and solving. Finally, we describe the first integrated incremental ASP system, iclingo, and provide an experimental evaluation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)
Kautz, H., Selman, B.: Planning as satisfiability. In: Proc. of ECAI 1992, pp. 359–363. Wiley, Chichester (1992)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N., Turner, H.: Nonmonotonic causal theories. Artificial Intelligence 153(1-2), 49–104 (2004)
Gelfond, M., Lifschitz, V.: Action languages. Electron. Trans. on AI 3(6), 193–210 (1998)
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: Proc. of IJCAI 2007. AAAI Press, Menlo Park (2007)
Oikarinen, E., Janhunen, T.: Modular equivalence for normal logic programs. In: Proc. of ECAI 2006, pp. 412–416. IOS Press, Amsterdam (2006)
Lifschitz, V., Turner, H.: Splitting a logic program. In: Proc. of ICLP, pp. 23–37. MIT Press, Cambridge (1994)
Brass, S., Dix, J.: Semantics of (disjunctive) logic programs based on partial evaluation. Journal of Logic Programming 40(1), 1–46 (1999)
Eiter, T., Fink, M., Tompits, H., Woltran, S.: Simplifying logic programs under uniform and strong equivalence. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS, vol. 2923, pp. 87–99. Springer, Heidelberg (2003)
Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157(1-2), 115–137 (2004)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science 89(4) (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Thiele, S. (2008). Engineering an Incremental ASP Solver. In: Garcia de la Banda, M., Pontelli, E. (eds) Logic Programming. ICLP 2008. Lecture Notes in Computer Science, vol 5366. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89982-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-89982-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89981-5
Online ISBN: 978-3-540-89982-2
eBook Packages: Computer ScienceComputer Science (R0)