Abstract
Stable Model Checking (MC) in Answer Set Programming systems is, in general, a co-NP task for disjunctive programs. Thus, implementing an efficient strategy is very important for the performance of ASP systems. In DLV, MC is carried out by exploiting the SAT solver SATZ, and the result of this operation also returns (in case the check fails) an ”unfounded set”, as by-product, which is also used for pruning the search space during answer set computation.
In this paper we report on the integration of a “modern” SAT solver, MiniSAT, in DLV. The integration poses not only technological issues, but also challenges w.r.t. the ”quality” of the returned unfounded set and w.r.t. the interplay with the existing DLV techniques.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Gelfond, M., Lifschitz, V.: The Stable Model Semantics for Logic Programming. In: ICLP/SLP 1988, pp. 1070–1080. MIT Press, Cambridge (1988)
Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Databases. NGC 9, 365–385 (1991)
Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. CUP (2003)
Lifschitz, V.: Action Languages, Answer Sets and Planning. In: The Logic Programming Paradigm – A 25-Year Perspective, pp. 357–373 (1999)
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV System for Knowledge Representation and Reasoning. ACM TOCL 7(3), 499–562 (2006)
Janhunen, T., Niemelä, I., Seipel, D., Simons, P., You, J.H.: Unfolding Partiality and Disjunctions in Stable Model Semantics. ACM TOCL 7(1), 1–37 (2006)
Lierler, Y.: Disjunctive Answer Set Programming via Satisfiability. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 447–451. Springer, Heidelberg (2005)
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: IJCAI 2007, pp. 386–392 (2007)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962)
Ben-Eliyahu, R., Dechter, R.: Propositional Semantics for Disjunctive Logic Programs. AMAI 12, 53–87 (1994)
Koch, C., Leone, N., Pfeifer, G.: Enhancing Disjunctive Logic Programming Systems by SAT Checkers. AI 15(1-2), 177–212 (2003)
Leone, N., Rullo, P., Scarcello, F.: Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics and Computation. Inf.Comp. 135(2), 69–112 (1997)
Pfeifer, G.: Improving the Model Generation/Checking Interplay to Enhance the Evaluation of Disjunctive Programs. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 220–233. Springer, Heidelberg (2003)
Janhunen, T., Niemelä, I., Simons, P., You, J.H.: Partiality and Disjunctions in Stable Model Semantics. In: KR 2000, vol. 12, 15, pp. 411–419 (2000)
Giunchiglia, E., Maratea, M.: Solving optimization problems with DLL. In: Proc. of the 17th European Conference on Artificial Intelligence (ECAI 2006). Frontiers in Artificial Intelligence and Applications, vol. 141, pp. 377–381. IOS Press, Amsterdam (2006)
Järvisalo, M., Junttila, T.A., Niemelä, I.: Unrestricted vs restricted cut in a tableau method for boolean circuits. Annals of Mathemathics and Artificial Intelligence 44(4), 373–399 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maratea, M., Ricca, F., Veltri, P. (2010). DLV MC: Enhanced Model Checking in DLV . In: Janhunen, T., Niemelä, I. (eds) Logics in Artificial Intelligence. JELIA 2010. Lecture Notes in Computer Science(), vol 6341. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15675-5_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-15675-5_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15674-8
Online ISBN: 978-3-642-15675-5
eBook Packages: Computer ScienceComputer Science (R0)