Skip to main content
SpringerLink
Log in
Book cover

International Conference on Logic Programming and Nonmonotonic Reasoning

LPNMR 2005: Logic Programming and Nonmonotonic Reasoning pp 240–252Cite as

Solving Hard ASP Programs Efficiently

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3662))

Abstract

Recent research on answer set programming (ASP) systems, has mainly focused on solving NP problems more efficiently. Yet, disjunctive logic programs allow for expressing every problem in the complexity classes \(\Sigma^P_2\) and \(\Pi^P_2\). These classes are widely believed to be strictly larger than NP, and several important AI problems, like conformant and conditional planning, diagnosis and more are located in this class.

In this paper we focus on improving the evaluation of \(\Sigma^P_2\)/\(\Pi^P_2\)-hard ASP programs. To this end, we define a new heuristic h DS and implement it in the (disjunctive) ASP system DLV. The definition of h DS is geared towards the peculiarites of hard programs, while it maintains the benign behaviour of the well-assessed heuristic of DLV for NP problems.

We have conducted extensive experiments with the new heuristic. h DS significantly outperforms the previous heuristic of DLV on hard 2QBF problems. We also compare the DLV system (with h DS ) to the QBF solvers SSolve, Quantor, Semprop, and yQuaffle, which performed best in the QBF evaluation of 2004. The results of the comparison indicate that ASP systems currently seem to be the best choice for solving \(\Sigma^P_2\)/\(\Pi^P_2\)-complete problems.

This work was supported by the European Commission under projects IST-2002-33570 INFOMIX, and IST-2001-37004 WASP.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Lifschitz, V.: Answer Set Planning. In: Schreye, D.D. (ed.) ICLP 1999, Las Cruces, New Mexico, USA, pp. 23–37. The MIT Press, Cambridge (1999)

    Google Scholar 

  2. Eiter, T., Gottlob, G., Mannila, H.: Disjunctive Datalog. ACM TODS 22, 364–418 (1997)

    Article  Google Scholar 

  3. Rintanen, J.: Improvements to the Evaluation of Quantified Boolean Formulae. In: Dean, T. (ed.) IJCAI 1999, Sweden, pp. 1192–1197 (1999)

    Google Scholar 

  4. Eiter, T., Gottlob, G.: The Complexity of Logic-Based Abduction. JACM 42, 3–42 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  5. Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. CUP (2002)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. Janhunen, T., Niemelä, I., Simons, P., You, J.H.: Partiality and Disjunctions in Stable Model Semantics. In: KR 2000, pp. 12–15, 411–419 (2000)

    Google Scholar 

  8. Koch, C., Leone, N., Pfeifer, G.: Enhancing Disjunctive Logic Programming Systems by SAT Checkers. Artificial Intelligence 15, 177–212 (2003)

    Article  MathSciNet  Google Scholar 

  9. Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV System for Knowledge Representation and Reasoning. ACM TOCL (2005) (to appear)

    Google Scholar 

  10. Simons, P., Niemelä, I., Soininen, T.: Extending and Implementing the Stable Model Semantics. Artificial Intelligence 138, 181–234 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  11. Lin, F., Zhao, Y.: ASSAT: Computing Answer Sets of a Logic Program by SAT Solvers. In: AAAI 2002, Edmonton, Alberta, Canada. AAAI Press / MIT Press (2002)

    Google Scholar 

  12. Lierler, Y., Maratea, M.: Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 346–350. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Faber, W., Leone, N., Pfeifer, G.: Experimenting with Heuristics for Answer Set Programming. In: IJCAI 2001, Seattle, WA, USA, pp. 635–640 (2001)

    Google Scholar 

  14. Cadoli, M., Giovanardi, A., Schaerf, M.: Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae. In: AI*IA 1997, Italy, pp. 207–218 (1997)

    Google Scholar 

  15. Gent, I., Walsh, T.: The QSAT Phase Transition. In: AAAI (1999)

    Google Scholar 

  16. Narizzano, M., Tacchella, A.: QBF Solvers Evaluation page (2002), http://www.qbflib.org/qbfeval/index.html/

  17. Berre, D.L., Simon, L., Tacchella, A.: Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 468–485. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Marek, W., Subrahmanian, V.: The Relationship between Logic Program Semantics and Non-Monotonic Reasoning. In: ICLP 1989, pp. 600–617. MIT Press, Cambridge (1989)

    Google Scholar 

  19. Leone, N., Rullo, P., Scarcello, F.: Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics and Computation. Information and Computation 135, 69–112 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  20. Baral, C., Gelfond, M.: Logic Programming and Knowledge Representation. JLP 19/20, 73–148 (1994)

    Article  MathSciNet  Google Scholar 

  21. Ben-Eliyahu, R., Dechter, R.: Propositional Semantics for Disjunctive Logic Programs. AMAI 12, 53–87 (1994)

    MATH  MathSciNet  Google Scholar 

  22. Faber, W., Leone, N., Pfeifer, G.: Pushing Goal Derivation in DLP Computations. In: Gelfond, M., Leone, N., Pfeifer, G. (eds.) LPNMR 1999. LNCS (LNAI), vol. 1730, p. 177. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  23. Eiter, T., Gottlob, G.: On the Computational Cost of Disjunctive Logic Programming: Propositional Case. AMAI 15, 289–323 (1995)

    MATH  MathSciNet  Google Scholar 

  24. Feldmann, R., Monien, B., Schamberger, S.: A Distributed Algorithm to Evaluate Quantified Boolean Formulae. In: Proceedings National Conference on AI (AAAI 2000), Austin, Texas, pp. 285–290. AAAI Press, Menlo Park (2000)

    Google Scholar 

  25. Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  27. Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  28. Cadoli, M., Eiter, T., Gottlob, G.: Default Logic as a Query Language. IEEE TKDE 9, 448–463 (1997)

    Google Scholar 

  29. Zolda, M.: Comparing Different Prenexing Strategies for Quantified Boolean Formulas. Master’s thesis, TU Wien (2005)

    Google Scholar 

  30. Castellini, C., Giunchiglia, E., Tacchella, A.: SAT-based planning in complex domains: Concurrency, constraints and nondeterminism. Artificial Intelligence 147, 85–117 (2003)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of Calabria, I-87030, Rende (CS), Italy

    Wolfgang Faber & Francesco Ricca

Authors
  1. Wolfgang Faber
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesco Ricca
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing and Informatics, Arizona State University, 85287-8809, Tempe, AZ

    Chitta Baral

  2. Dipartimento di Matematica, Università della Calabria, I-87036, Rende, CS, Italy

    Gianluigi Greco  & Giorgio Terracina  & 

  3. Department of Mathematics, University of Calabria, 87036, Rende, CS, Italy

    Nicola Leone

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Faber, W., Ricca, F. (2005). Solving Hard ASP Programs Efficiently. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2005. Lecture Notes in Computer Science(), vol 3662. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11546207_19

Download citation

  • DOI: https://doi.org/10.1007/11546207_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28538-0

  • Online ISBN: 978-3-540-31827-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation