Abstract
Propositional satisfiability (SAT) solvers provide a promising computational platform for logic programs under the stable model semantics. Computing stable models of a logic program using a SAT solver presumes translating the program into a set of clauses in the DIMACS format which is accepted by most SAT solvers as input. In this paper, we present succinct translations from programs with choice rules, cardinality rules, and weight rules—also known as smodels programs—to sets of clauses. These translations enable us to harness SAT solvers as black boxes to the task of computing stable models for logic programs generated by any smodels compatible grounder such as lparse or gringo. In the experimental part of this paper, we evaluate the potential of SAT solver technology in finding stable models using NP-complete benchmark problems employed in the Second Answer Set Programming Competition.
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
Apt, K., Blair, H., Walker, A.: Towards a theory of declarative knowledge. In: Foundations of Deductive Databases and Logic Programming, pp. 89–148. Morgan Kaufmann, San Francisco (1988)
Ben-Eliyahu, R., Dechter, R.: Propositional Semantics for Disjunctive Logic Programs. Annals of Mathematics and Artificial Intelligence 12(1-2), 53–87 (1994)
Clark, K.: Negation as failure. In: Logic and Data Bases, pp. 293–322. Plenum Press, New York (1978)
Denecker, M., Vennekens, J., Bond, S., Gebser, M., Truszczyński, M.: The second answer set programming competition. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 637–654. Springer, Heidelberg (2009)
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1-4), 1–26 (2006)
Erdem, E., Lifschitz, V.: Tight logic programs. Theory and Practice of Logic Programming 3(4-5), 499–518 (2003)
Ferraris, P., Lifschitz, V.: Weight constraints as nested expressions. Theory and Practice of Logic Programming 5(1-2), 45–74 (2005)
Gebser, M., Kaufmann, B., Schaub, T.: The conflict-driven answer set solver clasp: Progress report. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 509–514. Springer, Heidelberg (2009)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proceedings of ICLP 1988, pp. 1070–1080 (1988)
Giunchiglia, E., Lierler, Y., Maratea, M.: Answer set programming based on propositional satisfiability. Journal of Automated Reasoning 36(4), 345–377 (2006)
Janhunen, T.: Representing normal programs with clauses. In: Proceedings of ECAI 2004, pp. 358–362 (2004)
Janhunen, T.: Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics 16(1-2), 35–86 (2006)
Janhunen, T., Niemelä, I., Sevalnev, M.: Computing stable models via reductions to difference logic. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 142–154. Springer, Heidelberg (2009)
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Scarcello, F.: The DLV System for Knowledge Representation and Reasoning. ACM Transactions on Computational Logic 7(3), 499–562 (2006)
Lierler, Y.: Cmodels – SAT-based disjunctive answer set solver. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 447–451. Springer, Heidelberg (2005)
Lifschitz, V.: Answer set planning. In: Proceedings of ICLP 1999, pp. 23–37 (1999)
Lifschitz, V., Tang, L.R., Turner, H.: Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence 25(3-4), 369–389 (1999)
Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: Proceedings of IJCAI 2003, pp. 853–858 (2003)
Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157(1-2), 115–137 (2004)
Marek, V., Truszczyński, M.: Stable models and an alternative logic programming paradigm. In: The Logic Programming Paradigm: a 25-Year Perspective, pp. 375–398. Springer, Heidelberg (1999)
Marek, V.W., Subrahmanian, V.S.: The relationship between stable, supported, default and autoepistemic semantics for general logic programs. Theoretical Computer Science 103, 365–386 (1992)
Niemelä, I.: Logic programming with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25(3-4), 241–273 (1999)
Niemelä, I.: Stable models and difference logic. Annals of Mathematics and Artificial Intelligence 53(1-4), 313–329 (2008)
Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence 138(1-2), 181–234 (2002)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967–1970, pp. 466–483. Springer, Heidelberg (1983)
Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. Journal of the ACM 38(3), 620–650 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Janhunen, T., Niemelä, I. (2011). Compact Translations of Non-disjunctive Answer Set Programs to Propositional Clauses. In: Balduccini, M., Son, T.C. (eds) Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning. Lecture Notes in Computer Science(), vol 6565. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20832-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-20832-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20831-7
Online ISBN: 978-3-642-20832-4
eBook Packages: Computer ScienceComputer Science (R0)